diff options
Diffstat (limited to 'src/Experiments/GenericFieldPow.v')
| -rw-r--r-- | src/Experiments/GenericFieldPow.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v index 33d524567..b3d83dbe8 100644 --- a/src/Experiments/GenericFieldPow.v +++ b/src/Experiments/GenericFieldPow.v @@ -129,7 +129,7 @@ Module F. Field_simplify_done : forall (H:x==y), field_simplify_done H. Ltac field_nsatz := repeat match goal with - [ H: (_:F) == _ |- _ ] => + [ H: _ == _ |- _ ] => match goal with | [ Ha : field_simplify_done H |- _ ] => fail | _ => idtac |