Fix for Coq 8.4

1 files changed, 5 insertions, 9 deletions

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 0b84dc4d1..ec4e89a3b 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -216,15 +216,11 @@ Module Extended.
         rewrite <- to_twisted_add_unopt.
         { pose proof (add_coordinates_opt_correct (coordinates P) (coordinates Q)).
           cbv [add add_unopt].
-          match goal with
-          | [ |- context[exist _ ?x ?p] ]
-            => generalize p; generalize dependent x
-          end.
-          match goal with
-          | [ |- context[exist ?P ?x (?p ?k)] ]
-            => generalize (p k);
-                 let H := fresh in intro H; change (P x) in H; revert H; generalize x
-          end.
+          do 2 match goal with
+               | [ |- context[exist _ ?x ?p] ]
+                 => first [ is_var p; fail 1
+                          | generalize p; generalize dependent x ]
+               end.
           clear add_coordinates_opt add_coordinates_opt_correct.
           cbv [to_twisted coordinates proj1_sig E.eq E.coordinates fst snd] in *.
           repeat match goal with