Continuation of r16346 on filtering local definitions. Refined

the "choose less dependent" constraint-solving heuristic so that
it is not disturbed by local definitions.

This is a quick fix. A deeper analysis of the structure of constraints
of the form ?x[args] = y, determining if variable y can itself be a
local def or not, and whether args can be let-ins aliasing other
variables, would allow to know if the fix needs to be refined further.

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

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index fe537c59a..cd9a4a12b 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -15,3 +15,16 @@ Print P.
 
 (* Check that plus is folded even if reduction is involved *)
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
+
+
+(* Check that the heuristic to solve constraints is not artificially
+   dependent on the presence of a let-in, and in particular that the
+   second [_] below is not inferred to be n, as if obtained by
+   first-order unification with [T n] of the conclusion [T _] of the
+   type of the first [_]. *)
+
+(* Note: exact numbers of evars are not important... *)
+
+Inductive T (n:nat) : Type := A : T n.
+Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n => _ _ : T n.