From ecf68d1ed251e2c6b4abd9e97400d3ab009d2925 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 27 Apr 2008 16:15:34 +0000 Subject: - 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/setoid_replace.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'tactics/setoid_replace.ml') 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; } -- cgit v1.2.3