Suite restructuration unification et division des problèmes

d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).



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

1 files changed, 28 insertions, 12 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 96facdef2..cfecbf319 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -383,6 +383,32 @@ let error_already_defined b =
         anomalylabstrm ""
           (str "Position " ++ int n ++ str" already defined")
 
+let rec similar_type_shapes t u =
+  let t,_ = decompose_app t and u,_ = decompose_app u in
+  match kind_of_term t, kind_of_term u with
+  | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2
+  | Const cst, Const cst' -> cst = cst'
+  | Var id, Var id' -> id = id'
+  | Ind ind, Ind ind' -> ind = ind'
+  | Rel n, Rel n' -> n = n'
+  | Sort s, Sort s' -> family_of_sort s = family_of_sort s'
+  | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c'
+  | _ -> false
+
+let clenv_unify_similar_types clenv t u =
+  if similar_type_shapes t u then 
+    try Processed, clenv_unify true CUMUL t u clenv 
+    with e when precatchable_exception e -> Coercible t, clenv
+  else Coercible t, clenv
+
+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 = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
+  let status,clenv'' = clenv_unify_similar_types clenv' c_typ k_typ in
+(*  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*)
+  { clenv'' with evd = meta_assign k (c,status) clenv''.evd }
+
 let clenv_match_args bl clenv =
   if bl = [] then
     clenv
@@ -390,25 +416,15 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,b,(sigma,c)) ->
+      (fun clenv (loc,b,(sigma,c as sc)) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  let c_typ = nf_betaiota (clenv_get_type_of clenv c) in
-	  let c_typ = clenv_hnf_constr clenv c_typ in
-	  let clenv = { clenv with evd = evar_merge clenv.evd sigma} in
-	  {clenv with evd = meta_assign k (c,Coercible c_typ) clenv.evd})
+	  clenv_assign_binding clenv k sc)
       clenv bl
 
-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 = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
-  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
-  { clenv' with evd = meta_assign k (c',Coercible c_typ) evd }
-
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
   let k =