deplacement de Discharge dans toplevel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 9 insertions, 19 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c756d6169f..b0ec976326 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -101,7 +101,7 @@ let declare_parameter id c =
  
 (* Constants. *)
 
-type constant_declaration = constant_entry * strength * bool
+type constant_declaration = constant_entry * strength
 
 let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
 
@@ -110,13 +110,13 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_constant (sp,((ce,_,_) as cd)) =
+let cache_constant (sp,((ce,_) as cd)) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
   declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
-let load_constant (sp,((ce,_,_) as cd)) =
+let load_constant (sp,((ce,_) as cd)) =
   declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
@@ -184,7 +184,7 @@ let is_constant sp =
   try let _ = Global.lookup_constant sp in true with Not_found -> false
 
 let constant_strength sp = 
-  let (_,stre,_) = Spmap.find sp !csttab in stre
+  let (_,stre) = Spmap.find sp !csttab in stre
 
 let is_variable id = 
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
@@ -294,8 +294,7 @@ let declare_eliminations sp i =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     declare_constant (id_of_string na)
-      ({ const_entry_body = c; const_entry_type = None },
-       NeverDischarge, false);
+      ({ const_entry_body = c; const_entry_type = None }, NeverDischarge);
     pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/declare.mli b/library/declare.mli
index f5c2dff07c..15722dbc0a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,7 +23,7 @@ type strength =
 type variable_declaration = constr * strength * bool
 val declare_variable : identifier -> variable_declaration -> unit
 
-type constant_declaration = constant_entry * strength * bool
+type constant_declaration = constant_entry * strength
 val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
diff --git a/library/discharge.ml b/library/discharge.ml
deleted file mode 100644
index 17a70b2095..0000000000
--- a/library/discharge.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-
-(* $Id$ *)
-
-open Declare
-
-let close_section _ s = Lib.close_section s
diff --git a/library/discharge.mli b/library/discharge.mli
deleted file mode 100644
index 34b8bd1c7f..0000000000
--- a/library/discharge.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* $Id$ *)
-
-val close_section : bool -> string -> unit
diff --git a/library/lib.ml b/library/lib.ml
index b9964a87f9..457a27f6e2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -132,7 +132,8 @@ let close_section s =
   lib_stk := before;
   add_entry sp (ClosedSection (s,after));
   add_frozen_state ();
-  pop_path_prefix ()
+  pop_path_prefix ();
+  (sp,after)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
diff --git a/library/lib.mli b/library/lib.mli
index 56bbcd59cf..3d87abe4db 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -34,7 +34,7 @@ val contents_after : section_path option -> library_segment
 (*s Opening and closing a section. *)
 
 val open_section : string -> section_path
-val close_section : string -> unit
+val close_section : string -> section_path * library_segment
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list