- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec

  "pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1


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

5 files changed, 31 insertions, 22 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index e7423c748..4d0318ba2 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -402,15 +402,17 @@ let clenv_unify_binding_type clenv c t u =
     with e when precatchable_exception e ->
       TypeNotProcessed, clenv, c
 
-let clenv_assign_binding clenv k (sigma,c) =
+let clenv_assign_binding use_types 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
+  let status,clenv'',c = 
+    if use_types then clenv_unify_binding_type clenv' c c_typ k_typ
+    else TypeNotProcessed, clenv, c in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
-let clenv_match_args bl clenv =
+let clenv_match_args use_types bl clenv =
   if bl = [] then
     clenv
   else
@@ -423,7 +425,7 @@ let clenv_match_args bl clenv =
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding clenv k sc)
+	  clenv_assign_binding use_types clenv k sc)
       clenv bl
 
 let clenv_constrain_last_binding c clenv =
@@ -431,15 +433,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 clenv k (Evd.empty,c)
+  clenv_assign_binding true clenv k (Evd.empty,c)
 
-let clenv_constrain_dep_args hyps_only bl clenv =
+let clenv_constrain_dep_args use_types 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 clenv occlist bl
+      List.fold_left2 (clenv_assign_binding use_types) clenv occlist bl
     else 
       error ("Not the right number of missing arguments (expected "
 	     ^(string_of_int (List.length occlist))^")")
@@ -447,18 +449,18 @@ let clenv_constrain_dep_args hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
+let make_clenv_binding_gen use_types hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args hyps_only largs clause
+      clenv_constrain_dep_args use_types hyps_only largs clause
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
+      clenv_match_args use_types lbind clause
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
+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
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index dfa751349..954e5607f 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -97,7 +97,8 @@ 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 : arg_bindings -> clausenv -> clausenv
+val clenv_match_args : bool (* unify types *) -> arg_bindings -> clausenv -> 
+  clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
@@ -106,9 +107,10 @@ 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 :
-  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
-   clausenv
+  bool -> int option -> evar_info sigma -> constr * constr -> 
+    open_constr bindings -> clausenv
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bd023721a..5a99adb5a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -160,7 +160,7 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
-  let inh_coerce_to_fail env evd rigidonly v c1 t =
+  let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
       raise NoCoercion
@@ -183,7 +183,7 @@ module Default = struct
   let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try (the_conv_x_leq env t c1 evd, v)
     with Reduction.NotConvertible ->
-    try inh_coerce_to_fail env evd rigidonly v c1 t
+    try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
       kind_of_term (whd_betadeltaiota env (evars_of evd) t),
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b140ad51a..90d6bb081 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,18 +120,21 @@ 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 default_no_delta_unify_flags = {
+let simple_apply_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly = false;
+  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
@@ -723,5 +726,6 @@ 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 *)
-      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
-
+      | _ ->
+	  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
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 1b8f9ccd8..8cfa20948 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,11 +17,12 @@ 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 default_no_delta_unify_flags : unify_flags
+val simple_apply_unify_flags : unify_flags
 
 (* The "unique" unification fonction *)
 val w_unify :