- 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

1 files changed, 0 insertions, 2 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index b5710c966..dc8ff2b9c 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;
 }