From 71f0f4a08b1f1fdace0e738a3a51d07193155fe4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 12:19:09 +0000
Subject: La table de pré-évaluation des constantes ne doit pas persister au
 discharge

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

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 07c48c81cd..51cfe4f89e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -51,7 +51,7 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = true }
+      Summary.survive_section = false }
 
 
 (* Check that c is an "elimination constant"
-- 
cgit v1.2.3