Generalized the use of evar candidates in type inference unification:

- use evar candidates instead of postponed conversion problems when
  it is known (according to the projection heuristic used) that an
  evar has only a fixed number of possible instances (as e.g. in
  equation ?n[x,x] = x, with x a variable);
- this allows to be more robust in solving remaining problems: if
  several instanciations exist, and one is not compatible with a previous
  instantiation made among several choices for another evar,
  backtracking is now possible;
- this allows in particular to fix regression #2670 (two postponed
  conversion problems solved in an inconsistent way);
- but this requires more code.

At the same time, a refactoring of the code has been made so as to
hopefully clarify the elementary pieces of the algorithm. For
instance, there are now generic functions for both applying a filter
and giving candidates. The filter is systematically generalized so as
to have the ccl of the evar well-typed even in situations where we
could try on the contrary to restrict the evars occurring in the
ccl.

Anyway, when the representation of instances will be optimized using
identity substitutions, it will no longer be useful to use the filter
to shorten the size of the instances. Then, the filters will have,
like candidates, the only role of restricting the search space for
potential solutions to the unification problems.

Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un]
up to conversion instead of up to unification. This (potententially)
looses constraints but this avoids looping at the time of considering
remaining problems and applying heuristics to them.

Also added printing of evar candidates in debugging evar printers

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

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2670.v b/test-suite/bugs/closed/shouldsucceed/2670.v
new file mode 100644
index 000000000..c401420e9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2670.v
@@ -0,0 +1,21 @@
+(* Check that problems with several solutions are solved in 8.4 as in 8.2 and 8.3 *)
+
+Inductive Fin: nat -> Set :=
+| first k : Fin (S k)
+| succ k: Fin k -> Fin (S k).
+
+Lemma match_sym_eq_eq: forall (n1 n2: nat)(f: Fin n1)(e: n1 = n2),
+f = match sym_eq e in (_ = l) return (Fin l) with refl_equal =>
+    match e in (_ = l) return (Fin l) with refl_equal => f end end.
+Proof.
+  intros n1 n2 f e.
+  (* Next line has a dependent and a non dependent solution *)
+  (* 8.2 and 8.3 used to choose the dependent one which is the one to make *)
+  (* the goal progress *)
+  refine (match e return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
+  (* Next line similarly has a dependent and a non dependent solution *)
+  refine (match e with refl_equal => _ end).
+  reflexivity.
+Qed.