diff options
Diffstat (limited to 'src/Algebra/Group.v')
| -rw-r--r-- | src/Algebra/Group.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index c1c514171..b053fc844 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms Crypto.Util.Relations Crypto.Util.Tactics. +Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*). Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Section BasicProperties. @@ -213,4 +213,4 @@ Section HomomorphismComposition. Global Instance is_homomorphism_compose_refl : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x)) := is_homomorphism_compose (fun x => reflexivity _). -End HomomorphismComposition.
\ No newline at end of file +End HomomorphismComposition. |