From fdd6a17b272995237c9f95fc465bb1ff6871bedc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 22:53:10 +0200
Subject: 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.
---
 test-suite/bugs/closed/4205.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/4205.v

(limited to 'test-suite')

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).
-- 
cgit v1.2.3