- Backtrack sur option with_types suite à confusion sur l'utilisation

  des types des with-bindings dans la 8.1 [ceux-ci étaient déjà
  utilisés et ce qui est vraiment nouveau est que l'unification est
  maintenant celle de evarconv alors que c'était avant un mélange
  d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je
  renonce à maintenir la compatibilité (on se retrouve donc avec un
  exemple qui fonctionne différement dans TermsConv.v de CoLoR).
- Robustesse accrue pour la nouvelle facilité de syntaxe de binding
  avec paramètre pour pose/set.



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

4 files changed, 20 insertions, 29 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 4d0318ba2f..e7423c748b 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -402,17 +402,15 @@ let clenv_unify_binding_type clenv c t u =
     with e when precatchable_exception e ->
       TypeNotProcessed, clenv, c
 
-let clenv_assign_binding use_types clenv k (sigma,c) =
+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 = 
-    if use_types then clenv_unify_binding_type clenv' c c_typ k_typ
-    else TypeNotProcessed, clenv, c 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 }
 
-let clenv_match_args use_types bl clenv =
+let clenv_match_args bl clenv =
   if bl = [] then
     clenv
   else
@@ -425,7 +423,7 @@ let clenv_match_args use_types bl clenv =
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding use_types clenv k sc)
+	  clenv_assign_binding clenv k sc)
       clenv bl
 
 let clenv_constrain_last_binding c clenv =
@@ -433,15 +431,15 @@ let clenv_constrain_last_binding c clenv =
   let k =
     try list_last all_mvs 
     with Failure _ -> error "clenv_constrain_with_bindings" in
-  clenv_assign_binding true clenv k (Evd.empty,c)
+  clenv_assign_binding clenv k (Evd.empty,c)
 
-let clenv_constrain_dep_args use_types hyps_only bl clenv =
+let clenv_constrain_dep_args hyps_only bl clenv =
   if bl = [] then
     clenv
   else
     let occlist = clenv_dependent hyps_only clenv in
     if List.length occlist = List.length bl then
-      List.fold_left2 (clenv_assign_binding use_types) clenv occlist bl
+      List.fold_left2 clenv_assign_binding clenv occlist bl
     else 
       error ("Not the right number of missing arguments (expected "
 	     ^(string_of_int (List.length occlist))^")")
@@ -449,18 +447,18 @@ let clenv_constrain_dep_args use_types hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen use_types hyps_only n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args use_types hyps_only largs clause
+      clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args use_types lbind clause
+      clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply use_types = make_clenv_binding_gen use_types true 
-let make_clenv_binding = make_clenv_binding_gen true false None
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
+let make_clenv_binding = make_clenv_binding_gen false None
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 954e5607f1..dfa7513495 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -97,8 +97,7 @@ val clenv_missing : clausenv -> metavariable list
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
 (* defines metas corresponding to the name of the bindings *)
-val clenv_match_args : bool (* unify types *) -> arg_bindings -> clausenv -> 
-  clausenv
+val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
@@ -107,10 +106,9 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 (* the arity of the lemma is fixed *)
 (* the optional int tells how many prods of the lemma have to be used *)
 (* use all of them if None *)
-(* boolean tells to unify immediately unifiable types of the bindings *)
 val make_clenv_binding_apply :
-  bool -> int option -> evar_info sigma -> constr * constr -> 
-    open_constr bindings -> clausenv
+  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
+   clausenv
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 216900bdbd..84f9330d3b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,21 +120,18 @@ let sort_eqns = unify_r2l
 type unify_flags = { 
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
-  use_types : bool;
   modulo_delta : Names.transparent_state;
 }
 
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
-  use_types = true;
   modulo_delta = full_transparent_state;
 }
 
-let simple_apply_unify_flags = {
+let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = false;
-  use_types = false;
+  use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
 }
 
@@ -726,6 +723,5 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 		    error "Cannot solve a second-order unification problem")
 	    
       (* General case: try first order *)
-      | _ ->
-	  if flags.use_types then w_typed_unify env cv_pb flags ty1 ty2 evd
-	  else w_unify_0 env cv_pb flags ty1 ty2 evd
+      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
+
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8cfa209480..1b8f9ccd8b 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,12 +17,11 @@ open Evd
 type unify_flags = { 
   modulo_conv_on_closed_terms : Names.transparent_state option; 
   use_metas_eagerly : bool;
-  use_types : bool;
   modulo_delta : Names.transparent_state;
 }
 
 val default_unify_flags : unify_flags
-val simple_apply_unify_flags : unify_flags
+val default_no_delta_unify_flags : unify_flags
 
 (* The "unique" unification fonction *)
 val w_unify :