Refining 71def2f8 on too strong occur-check limiting evar-evar

unification in tactics.

The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.

Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.

1 files changed, 8 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v
new file mode 100644
index 0000000000..c40dfcc1f3
--- /dev/null
+++ b/test-suite/bugs/closed/4205.v
@@ -0,0 +1,8 @@
+(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
+
+
+Inductive test : nat -> nat -> nat -> nat -> Prop :=
+  | test1 : forall m n, test m n m n.
+
+Goal test 1 2 3 4.
+erewrite f_equal2 with (f := fun k l => test _ _ k l).