Unification: Added a heuristic to solve problems of the form

?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to
know if it occurs in rigid position or not. Such equations typically
come from matching problems such as "match a return ?T[a] with pair a1
a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the
return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified
with ?A.  This possible dependency is kept since commits r15060-15062.
The heuristic is to restrict ?T so that the dependency is removed,
leading to a behavior similar to the one existing before these commits.

This allows BGsection15.v, from contrib Ssreflect, to compile as it
did before these commits.

Also, removed one function exported without true need in r15061.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 906eb0fc9..e6088091b 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -367,3 +367,15 @@ Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _))
            (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
 
 End Bigop.
+
+(* Check the use of (at least) an heuristic to solve problems of the form
+   "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can
+   eventually be erased in t *)
+
+Section evar_evar_occur.
+  Variable id : nat -> nat.
+  Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2.
+  Variable g : forall y, id y = 0 /\ id y = 0.
+  (* Still evars in the resulting type, but constraints should be solved *)
+  Check match g _ with conj a b => f _ a b end.
+End evar_evar_occur.