Skip to content

Commit acfae5f

Browse files
committed
1 parent 41ce350 commit acfae5f

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

theories/tactics.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
22
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
33
From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
4-
From mathcomp Require Export zify ring.
4+
From mathcomp Require Export zify.
5+
From mathcomp.algebra_tactics Require Export ring.
56

67
Set Implicit Arguments.
78
Unset Strict Implicit.

0 commit comments

Comments
 (0)