Don't rely on autogenerated names

This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).

4 files changed, 20 insertions, 8 deletions

diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
index e77e39f50..8e69b78fe 100644
--- a/src/Curves/Edwards/AffineProofs.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -44,7 +44,7 @@ Module E.
     Local Notation mul   := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
 
     Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
-    Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed.
+    Next Obligation. match goal with P : point |- _ => destruct P as [ [??]?] end; cbv; fsatz. Qed.
 
     Ltac t_step :=
       match goal with
@@ -203,7 +203,10 @@ Module E.
         cbv [compress decompress exist_option coordinates] in *; intros.
         t.
         intro.
-        apply (H0 f); [|congruence].
+        match goal with
+        | [ H0 : _ |- False ]
+          => apply (H0 f); [|congruence]
+        end.
         admit.
         intro. Prod.inversion_prod; subst.
         rewrite solve_correct in y.
diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
index 2b126dfcb..3604e9b2e 100644
--- a/src/Curves/Edwards/XYZT.v
+++ b/src/Curves/Edwards/XYZT.v
@@ -105,7 +105,12 @@ Module Extended.
           let Z3 := F*G in
           (X3, Y3, Z3, T3)
         end.
-      Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
+      Next Obligation.
+        match goal with
+        | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
+          => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2)))
+        end; t.
+      Qed.
 
       Global Instance isomorphic_commutative_group_m1 :
         @Group.isomorphic_commutative_groups
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index bfd7dce60..2e39c6b6c 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -2,6 +2,7 @@ Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings.
 Require Import Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
 
 Module M.
@@ -30,7 +31,7 @@ Module M.
       | (x, y) => (x, -y)
       | ∞ => ∞
       end.
-    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+    Next Obligation. Proof. destruct_head @M.point; cbv; break_match; trivial; fsatz. Qed.
 
     Local Notation add := (M.add(b_nonzero:=b_nonzero)).
     Local Notation point := (@M.point F Feq Fadd Fmul a b).
@@ -52,14 +53,14 @@ Module M.
         | (x, y) => ((x + a/3)/b, y/b)
         | _ => ∞
         end.
-      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+      Next Obligation. Proof. destruct_head' @point; cbv; break_match; trivial; fsatz. Qed.
 
       Program Definition of_Weierstrass (P:Wpoint) : point :=
         match W.coordinates P return F*F+∞ with
         | (x,y) => (b*x-a/3, b*y)
         | _ => ∞
         end.
-      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+      Next Obligation. Proof. destruct_head' @Wpoint; cbv; break_match; trivial; fsatz. Qed.
     End MontgomeryWeierstrass.
   End MontgomeryCurve.
 End M.
diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v
index 20866ca5d..3c1fd204d 100644
--- a/src/Curves/Weierstrass/Projective.v
+++ b/src/Curves/Weierstrass/Projective.v
@@ -123,8 +123,11 @@ Module Projective.
       end.
     Next Obligation.
     Proof.
-      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
-      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      match goal with
+      | [ |- match (let (_, _) := proj1_sig ?P in let (_, _) := _ in let (_, _) := proj1_sig ?Q in _) with _ => _ end ]
+        => destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1];
+             destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2]
+      end.
       t.
       all: try abstract fsatz.
       (* FIXME: the final fsatz starts requiring 56 <> 0 if