Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le

lemme n'est pas un lemme d'induction (plus précisément si la tête de
la conclusion n'est pas une variable), alors on n'instancie pas les
with-bindings pour que les unifications venant du filtrage de la
conclusion du lemme avec le but soient prioritaires (en effet
l'utilisation des types des with-bindings pour inférer des instances
-- portion du commit r9842 -- ne produit pas des solutions exactes
mais seulement des sous-types de solutions exactes alors que
l'unification avec le but produit des solutions exactes qui doivent
donc être considérées en priorité). Toutefois, dans certains cas, du
fait que unify_0 travaille modulo conversion uniquement sur les termes
clos, il faut quand même donner crédit aux instances données en
with-bindings pour que la conversion puisse être prise en compte et
ainsi retrouver un comportement au moins identique au précédent.


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

4 files changed, 34 insertions, 38 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 929535b76b..c563688a8b 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -67,13 +67,7 @@ let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c =
-  let metamap =
-    List.map 
-      (function
-	 | (n,Clval(_,_,typ)) -> (n,typ.rebus)
-         | (n,Cltyp (_,typ))    -> (n,typ.rebus))
-      (meta_list ce.evd) in
-  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
+  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) (metas_of ce.evd) c
 
 exception NotExtensibleClause
 
@@ -255,8 +249,11 @@ let clenv_unify allow_K cv_pb t1 t2 clenv =
   { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }
 
 let clenv_unique_resolver allow_K clenv gl =
-  clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
-
+  if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
+    clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+  else
+    try clenv_unify allow_K CUMUL clenv.templtyp.rebus (pf_concl gl) clenv
+    with _ -> clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
 
 (* [clenv_pose_dependent_evars clenv]
  * For each dependent evar in the clause-env which does not have a value,
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d959be8bd..1ff0c633a0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -464,6 +464,12 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
 
 let meta_list evd = metamap_to_list evd.metas
 
+let metas_of evd = 
+  List.map (function
+    | (n,Clval(_,_,typ)) -> (n,typ.rebus)
+    | (n,Cltyp (_,typ))  -> (n,typ.rebus))
+    (meta_list evd)
+
 let meta_defined evd mv =
   match Metamap.find mv evd.metas with
     | Clval _ -> true
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f6052b3686..a1323e501c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -15,6 +15,7 @@ open Term
 open Sign
 open Libnames
 open Mod_subst
+open Termops
 (*i*)
 
 (* The type of mappings for existential variables.
@@ -174,6 +175,8 @@ val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> ev
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
 
+val metas_of : evar_defs -> metamap
+
 (**********************************************************)
 (* Sort variables *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d991486c40..5231cce429 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -23,6 +23,7 @@ open Rawterm
 open Pattern
 open Evarutil
 open Pretype_errors
+open Retyping
 
 (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
    gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
@@ -86,7 +87,7 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
 	(k,solve_pattern_eqn env (Array.to_list l) c,pb)::metasubst,evarsubst
     | Evar ev ->
       (* Currently unused: incompatible with eauto/eassumption backtracking *)
-	metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+	metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
     | _ -> assert false
 
 (*******************************)
@@ -136,8 +137,8 @@ let unify_0 env sigma cv_pb mod_delta m n =
 	    if (closedn (nb_rel env) cM)
 	    then (k,cM,fst (extract_instance_status pb))::metasubst,evarsubst
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
-	| Evar _, _ -> metasubst,((cM,cN)::evarsubst)
-	| _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+	| Evar ev, _ -> metasubst,((ev,cN)::evarsubst)
+	| _, Evar ev -> metasubst,((ev,cM)::evarsubst)
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
 	    unirec_rec (push_rel_assum (na,t1) curenv) topconv
 	      (unirec_rec curenv topconv substn t1 t2) c1 c2
@@ -319,20 +320,18 @@ let w_merge env with_types mod_delta metas evars evd =
   let ty_evars = ref [] in
   let rec w_merge_rec evd metas evars =
     match (evars,metas) with
-      | ([], []) -> evd
+    | [], [] -> evd
 
-      | ((lhs,rhs)::t, metas) ->
-      (match kind_of_term rhs with
+    | ((evn,_ as ev),rhs)::t, metas ->
+	(match kind_of_term rhs with
 
-	| Meta k -> w_merge_rec evd ((k,lhs,ConvUpToEta 0)::metas) t
+	| Meta k -> w_merge_rec evd ((k,mkEvar ev,ConvUpToEta 0)::metas) t
 
 	| krhs ->
-        (match kind_of_term lhs with
-
-	  | Evar (evn,_ as ev) ->
     	      if is_defined_evar evd ev then
+		let v = Evd.existential_value (evars_of evd) ev in
 		let (metas',evars') =
-                  unify_0 env (evars_of evd) topconv mod_delta rhs lhs in
+		  unify_0 env (evars_of evd) topconv mod_delta rhs v in
 		w_merge_rec evd (metas'@metas) (evars'@t)
     	      else begin
 		let rhs' =
@@ -352,9 +351,7 @@ let w_merge env with_types mod_delta metas evars evd =
                   | _ ->
                       (* ensure tail recursion in non-mimickable case! *)
 		      w_merge_rec (fst (evar_define env ev rhs' evd)) metas t
-	      end
-
-	  | _ -> anomaly "w_merge_rec"))
+	      end)
 
       | ([], (mv,n,status)::t) ->
     	  if meta_defined evd mv then
@@ -368,26 +365,19 @@ let w_merge env with_types mod_delta metas evars evd =
             w_merge_rec evd' (metas'@t) evars'
     	  else
 	    begin
+	      let evd' = meta_assign mv (n,status) evd in
 	      if with_types (* or occur_meta mvty *) then
 		begin
-	          let mvty = Typing.meta_type evd mv in
+	          let mvty = Typing.meta_type evd' mv in
 		  try 
-                    let sigma = evars_of evd in
-                    (* why not typing with the metamap ? *)
-		    let nty = Typing.type_of env sigma (nf_meta evd n) in
-		    (* unification with arities may induce a too early *)
-		    (* commitment of an evar to an arity of wrong sort *)
-		    if
-		      not (is_arity env sigma mvty) &&
-		      not (is_arity env sigma nty)
-		    then
-		      let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty
-		      in
-                      ty_metas := mc @ !ty_metas;
-                      ty_evars := ec @ !ty_evars
+                    let sigma = evars_of evd' in
+		    let metas = metas_of evd' in
+		    let nty = get_type_of_with_meta env sigma metas (nf_meta evd' n) in
+		    let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty in
+                    ty_metas := mc @ !ty_metas;
+                    ty_evars := ec @ !ty_evars
 		  with e when precatchable_exception e -> ()
 		end;
-	      let evd' = meta_assign mv (n,status) evd in
 	      w_merge_rec evd' t []
 	    end