aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra/Field.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Algebra/Field.v')
-rw-r--r--src/Algebra/Field.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index 7270f6018..b5b65f161 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -186,7 +186,7 @@ Section Homomorphism_rev.
| [ H : field |- _ ] => destruct H; try clear H
| [ H : commutative_ring |- _ ] => destruct H; try clear H
| [ H : ring |- _ ] => destruct H; try clear H
- | [ H : abelian_group |- _ ] => destruct H; try clear H
+ | [ H : commutative_group |- _ ] => destruct H; try clear H
| [ H : group |- _ ] => destruct H; try clear H
| [ H : monoid |- _ ] => destruct H; try clear H
| [ H : is_commutative |- _ ] => destruct H; try clear H