[ssr] Remove the unify_helper tactic that appears unnecessary

It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.

2 files changed, 12 insertions, 34 deletions

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index c78381d3cc..e1e4d25ced 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -528,28 +528,6 @@ Parameter under_done :
   forall (T : Type) (x : T), @Under T x x.
 Notation "''Under[' x ]" := (@Under _ x _)
   (at level 8, format "''Under['  x  ]").
-
-Ltac beta_expand c e :=
-  match e with
-  | ?G ?z =>
-    let T := type of z in
-    match c with
-    | context f [z] =>
-      let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in
-      rewrite -{1}[c]/(b z); beta_expand b G
-    | (* constante *) _ =>
-      let b := constr:(fun x : T => ltac:(exact c)) in
-      rewrite -{1}[c]/(b z); beta_expand b G
-    end
-  | ?G => idtac
-  end.
-
-Ltac unify_helper :=
-  move=> *;
-  lazymatch goal with
-  | [ |- @Under _ ?c ?e ] =>
-    beta_expand c e
-  end.
 End UNDER.
 
 Module Export Under : UNDER.
@@ -575,7 +553,6 @@ Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 Ltac over :=
   solve [ apply Under.under_done
         | by rewrite over
-        | unify_helper; eapply Under.under_done
         ].
 
 (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
index 3bb5c03e08..cd6b196eeb 100644
--- a/test-suite/ssr/over.v
+++ b/test-suite/ssr/over.v
@@ -4,10 +4,11 @@ Axiom daemon : False. Ltac myadmit := case: daemon.
 
 (** Testing over for the 1-var case *)
 
-Lemma test_over_1_1 : forall i : nat, False.
+Lemma test_over_1_1 : False.
 intros.
 evar (I : Type); evar (R : Type); evar (x2 : I -> R).
-assert (H : i + 2 * i - i = x2 i).
+assert (H : forall i : nat, i + 2 * i - i = x2 i).
+  intros i.
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
@@ -18,10 +19,11 @@ assert (H : i + 2 * i - i = x2 i).
   myadmit.
 Qed.
 
-Lemma test_over_1_2 : forall i : nat, False.
+Lemma test_over_1_2 : False.
 intros.
 evar (I : Type); evar (R : Type); evar (x2 : I -> R).
-assert (H : i + 2 * i - i = x2 i).
+assert (H : forall i : nat, i + 2 * i - i = x2 i).
+  intros i.
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
@@ -34,10 +36,11 @@ Qed.
 
 (** Testing over for the 2-var case *)
 
-Lemma test_over_2_1 : forall i j : nat, False.
+Lemma test_over_2_1 : False.
 intros.
 evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
-assert (H : i + 2 * j - i = x2 i j).
+assert (H : forall i j, i + 2 * j - i = x2 i j).
+  intros i j.
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold J in *; clear J;
@@ -49,10 +52,11 @@ assert (H : i + 2 * j - i = x2 i j).
   myadmit.
 Qed.
 
-Lemma test_over_2_2 : forall i j : nat, False.
+Lemma test_over_2_2 : False.
 intros.
 evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
-assert (H : i + 2 * j - i = x2 i j).
+assert (H : forall i j : nat, i + 2 * j - i = x2 i j).
+  intros i j.
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold J in *; clear J;
@@ -61,9 +65,6 @@ assert (H : i + 2 * j - i = x2 i j).
   Fail done.
 
   rewrite over.
-  Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *)
-  rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j).
-  (* cf. [plugins/ssr/ssreflect.v:unify_helper] *)
   done.
   myadmit.
 Qed.