- 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

5 files changed, 5 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 111245e117..0b1f29dc3b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -586,7 +586,6 @@ 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 72bc85c2f4..4319a1d3de 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -72,7 +72,6 @@ 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;
 }
 
@@ -632,7 +631,6 @@ 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;
 }
 
@@ -641,7 +639,6 @@ 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 b5710c9666..dc8ff2b9cd 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,14 +1734,12 @@ 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 1bd65ecdf6..dd8aa12941 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 true indbindings indclause in
+  let indclause' = clenv_match_args 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 true elimbindings elimclause' in
+  let elimclause' = clenv_match_args 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 cd8ad4c14d..d3f7cc5f15 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -551,7 +551,6 @@ 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;
 }
 
@@ -673,10 +672,9 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl =
+let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if with_delta_and_types then default_unify_flags
-    else simple_apply_unify_flags in
+    if with_delta then default_unify_flags else default_no_delta_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. *)
@@ -686,9 +684,7 @@ let general_apply with_delta_and_types 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 with_delta_and_types (Some n) gl (c,thm_ty) lbind
-    in
+    let clause = make_clenv_binding_apply gl (Some n) (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 ->