From c88af9ff3deaa6da8985c5119284b7a925a04d65 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 28 Feb 2001 09:33:03 +0000
Subject: bug Reset et Sections

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

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 53b5a21b04..10fd9b9655 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -160,7 +160,6 @@ let close_section export s =
   pop_path_prefix ();
   add_entry 
     (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after'));
-  add_frozen_state ();
   (sp,after,fs)
 
 (* The following function exports the whole library segment, that will be 
diff --git a/library/lib.mli b/library/lib.mli
index bc4032a61d..668a65adf9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -28,6 +28,7 @@ and library_segment = library_entry list
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
+val add_frozen_state : unit -> unit
 
 
 (*s The function [contents_after] returns the current library segment, 
-- 
cgit v1.2.3