Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk

(résolution entre autres des bugs 1882, 1883, 1884).



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

4 files changed, 28 insertions, 18 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index e7423c748..074dd0901 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -406,7 +406,6 @@ let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
   let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
-  let c_typ = clenv_hnf_constr clenv' c_typ in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5edd6054..58e9aca9e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -492,10 +492,12 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       else
 	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
 
-let choose_less_dependent_instance evk evd =
+let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
-  let ctx = evar_filtered_context evi in
-  Evd.evar_define evk (mkVar (pi1 (List.hd ctx))) evd
+  let subst = make_pure_subst evi args in
+  let subst' = List.filter (fun (id,c) -> c = term) subst in
+  if subst' = [] then error "Too complex unification problem" else
+  Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
   let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in
@@ -506,13 +508,13 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
   | Evar (evk1,args1), Rel _ when l1 = [] & l2 = [] ->
       (* The typical kind of constraint coming from patter-matching return
          type inference *)
-      assert (array_for_all ((=) term2) args1);
-      choose_less_dependent_instance evk1 evd, true
+      assert (array_for_all (fun a -> a = term2 or isEvar a) args1);
+      choose_less_dependent_instance evk1 evd term2 args1, true
   | Rel _, Evar (evk2,args2) when l1 = [] & l2 = [] ->
       (* The typical kind of constraint coming from patter-matching return
          type inference *)
       assert (array_for_all ((=) term1) args2);
-      choose_less_dependent_instance evk2 evd, true
+      choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       first_order_unification env evd (ev1,l1) appr2
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9a9d75eb8..27e964b6a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -48,6 +48,8 @@ val e_new_evar :
 val new_evar_instance :
  named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr
 
+val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
+
 (***********************************************************)
 (* Instantiate evars *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 41d6ff4c1..108e21f67 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -406,19 +406,26 @@ let pose_all_metas_as_evars env evd t =
   (* side-effect *)
   (!evdref, c)
 
+let try_to_coerce env evd c cty tycon =
+  let j = make_judge c cty in
+  let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+  let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
+  if b then
+    let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
+    (evd',j'.uj_val)
+  else
+    error "Cannot solve unification constraints"
+
 let w_coerce_to_type env evd c cty mvty =
-  try
-    let j = make_judge c cty in
-    let evd,mvty = pose_all_metas_as_evars env evd mvty in
-    let tycon = mk_tycon_type mvty in
-    let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
-    let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
-    if b then
-      let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
-      (evd',j'.uj_val)
-    else (evd,c)
+  let evd,mvty = pose_all_metas_as_evars env evd mvty in
+  let tycon = mk_tycon_type mvty in
+  try try_to_coerce env evd c cty tycon
   with e when precatchable_exception e ->
-    (evd,c)
+    (* inh_conv_coerce_rigid_to should have reasoned modulo reduction 
+       but there are cases where it though it was not rigid (like in
+       fst (nat,nat)) and stops while it could have seen that it is rigid *)
+    let cty = Tacred.hnf_constr env (evars_of evd) cty in
+    try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
   let cty = get_type_of env (evars_of evd) c in