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

1 files changed, 2 insertions, 0 deletions

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". *)