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.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenvtac.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index babf53c9fb..22dcca2890 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -98,7 +98,6 @@ open Unification
 let fail_quick_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
-  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
-- 
cgit v1.2.3