From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 24 Nov 2000 16:13:28 +0000
Subject: certains effets disparaissent a la sortie des sections, d'autres non
 (selon Summary.survive_section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml     | 3 ++-
 tactics/dhyp.ml     | 3 ++-
 tactics/equality.ml | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 27b04eedb0..70ff2e6395 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -142,7 +142,8 @@ let unfreeze fs = searchtable := fs
 let _ = Summary.declare_summary "search"
 	  { Summary.freeze_function   = freeze;
 	    Summary.unfreeze_function = unfreeze;
-	    Summary.init_function     = init }
+	    Summary.init_function     = init;
+	    Summary.survive_section   = false }
 
  
 (**************************************************************************)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 628c337f90..6497287ab5 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -177,7 +177,8 @@ let _ =
   Summary.declare_summary "destruct-hyp-concl"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let cache_dd (_,(na,dd)) =
   try 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a901146416..96c323d733 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1574,7 +1574,8 @@ let _ =
   Summary.declare_summary "autorewrite"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = false }
 
 (*Adds a list of rules to the rule table*)
 let add_list_rules rbase lrl = 
-- 
cgit v1.2.3