- 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, 15 insertions, 5 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 66fde8f6b..8823efe0b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -586,6 +586,7 @@ open Unification
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
+  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4319a1d3d..72bc85c2f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -72,6 +72,7 @@ open Unification
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = var_full_transparent_state;
 }
 
@@ -631,6 +632,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
+  Unification.use_types = true;
   Unification.modulo_delta = empty_transparent_state;
 }
 
@@ -639,6 +641,7 @@ let conv_transparent_state = (Idpred.empty, Cpred.full)
 let rewrite2_unif_flags = {
   Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
   Unification.use_metas_eagerly = true;
+  Unification.use_types = true;
   Unification.modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index dc8ff2b9c..b5710c966 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,12 +1734,14 @@ let check_evar_map_of_evars_defs evd =
 let rewrite_unif_flags = {
   modulo_conv_on_closed_terms = None;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
 let rewrite2_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dd8aa1294..1bd65ecdf 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -329,7 +329,7 @@ let general_elim_then_using mk_elim
   ind indclause gl =
   let elim = mk_elim ind gl in
   (* applying elimination_scheme just a little modified *)
-  let indclause' = clenv_match_args indbindings indclause in
+  let indclause' = clenv_match_args true indbindings indclause in
   let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
@@ -350,7 +350,7 @@ let general_elim_then_using mk_elim
 	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
-  let elimclause' = clenv_match_args elimbindings elimclause' in
+  let elimclause' = clenv_match_args true elimbindings elimclause' in
   let branchsigns = compute_construtor_signatures isrec ind in
   let brnames = compute_induction_names (Array.length branchsigns) allnames in
   let after_tac ce i gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d3f7cc5f1..cd8ad4c14 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -551,6 +551,7 @@ let last_arg c = match kind_of_term c with
 let elim_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
@@ -672,9 +673,10 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let general_apply with_delta with_destruct with_evars (c,lbind) gl =
+let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if with_delta then default_unify_flags else default_no_delta_unify_flags in
+    if with_delta_and_types then default_unify_flags
+    else simple_apply_unify_flags in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
@@ -684,7 +686,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let try_apply thm_ty nprod =
     let n = nb_prod thm_ty - nprod in
     if n<0 then error "Apply: theorem has not enough premisses.";
-    let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+    let clause =
+     make_clenv_binding_apply with_delta_and_types (Some n) gl (c,thm_ty) lbind
+    in
     Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
   try try_apply thm_ty0 concl_nprod
   with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->