From e7f9bc39ab4e879b521439901ed99bf3382bd40a Mon Sep 17 00:00:00 2001
From: coq
Date: Tue, 7 Oct 2003 15:36:10 +0000
Subject: Correction du bug 335 et Export/Require Export dans un module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml           | 1 +
 tactics/autorewrite.ml    | 1 +
 tactics/dhyp.ml           | 1 +
 tactics/setoid_replace.ml | 2 ++
 tactics/tacinterp.ml      | 1 +
 5 files changed, 6 insertions(+)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c7186e4123..4683ce1447 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -159,6 +159,7 @@ let _ = Summary.declare_summary "search"
 	  { Summary.freeze_function   = freeze;
 	    Summary.unfreeze_function = unfreeze;
 	    Summary.init_function     = init;
+	    Summary.survive_module = false;
 	    Summary.survive_section   = false }
 
  
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 7febf87ab9..a0f0f72269 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -36,6 +36,7 @@ let _ =
     { Summary.freeze_function   = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function     = init;
+      Summary.survive_module = false;
       Summary.survive_section   = false }
 
 (* Rewriting rules before tactic interpretation *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 252e302c2c..fc20b9c76e 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -196,6 +196,7 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
+      Summary.survive_module = false;
       Summary.survive_section = false }
 
 let forward_subst_tactic = 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 3efd23f6a1..0ff8ba69a3 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -111,6 +111,7 @@ let _ =
     { Summary.freeze_function = (fun () -> !setoid_table);
       Summary.unfreeze_function = (fun t -> setoid_table := t);
       Summary.init_function = (fun () -> setoid_table := Gmap .empty);
+      Summary.survive_module = false;
       Summary.survive_section = false }
 
 (* Declare a new type of object in the environment : "setoid-theory". *)
@@ -163,6 +164,7 @@ let _ =
     { Summary.freeze_function = (fun () -> !morphism_table);
       Summary.unfreeze_function = (fun t -> morphism_table := t);
       Summary.init_function = (fun () -> morphism_table := Gmap .empty);
+      Summary.survive_module = false;
       Summary.survive_section = false }
 
 (* Declare a new type of object in the environment : "morphism-definition". *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 619d26c619..0f2bf9ca92 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -250,6 +250,7 @@ let _ =
     { Summary.freeze_function   = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function     = init;
+      Summary.survive_module = false;
       Summary.survive_section   = false }
 
 (* Interpretation of extra generic arguments *)
-- 
cgit v1.2.3