From cf6388889773447a8e2727c30c982ea3399db29b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 23 Apr 2008 07:35:14 +0000
Subject: Backtrack on change of flags for elim, otherwise rewrite goes under
 local variables...

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ac83467a4a..34c2f690c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -551,7 +551,7 @@ 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;
-  modulo_delta = var_full_transparent_state;
+  modulo_delta = empty_transparent_state;
 }
 
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
-- 
cgit v1.2.3