From fc10282837971f8f0648841d944dd64b11d3a3db Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 26 Apr 2008 12:31:25 +0000
Subject: - 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
---
 proofs/clenvtac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 22dcca2890..babf53c9fb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -98,6 +98,7 @@ 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