Intégration des modifs de la branche mowgli :

- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
  Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
  (nouveau fichier library/dischargedhypsmap.ml).


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

8 files changed, 271 insertions, 114 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
new file mode 100644
index 000000000..566da65d6
--- /dev/null
+++ b/library/decl_kinds.ml
@@ -0,0 +1,67 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Informal mathematical status of declarations *)
+
+(* Kinds used at parsing time *)
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+
+type locality_flag = (*bool (* local = true; global = false *)*)
+  | Local
+  | Global
+
+type strength = locality_flag (* For compatibility *)
+
+type type_as_formula_kind = Definitional | Logical
+
+(* [assumption_kind] 
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+*)
+type assumption_kind = locality_flag * type_as_formula_kind
+
+type definition_kind = locality_flag
+
+(* Kinds used in proofs *)
+
+type global_goal_kind =
+  | DefinitionBody
+  | Proof of theorem_kind
+
+type goal_kind =
+  | IsGlobal of global_goal_kind
+  | IsLocal
+
+(* Kinds used in library *)
+
+type local_theorem_kind = LocalStatement
+
+type 'a mathematical_kind =
+  | IsAssumption of type_as_formula_kind
+  | IsDefinition
+  | IsProof of 'a
+
+type global_kind = theorem_kind mathematical_kind
+type local_kind = local_theorem_kind mathematical_kind
+
+(* Utils *)
+
+let theorem_kind_of_goal_kind = function
+  | DefinitionBody -> IsDefinition
+  | Proof s -> IsProof s
+
diff --git a/library/declare.ml b/library/declare.ml
index b338277d3..b67dbc6e2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -28,6 +28,7 @@ open Impargs
 open Nametab
 open Library
 open Safe_typing
+open Decl_kinds
 
 (**********************************************)
 
@@ -39,38 +40,23 @@ open Safe_typing
 
 open Nametab
 
-let depth_of_strength = function
-  | DischargeAt (sp',n) -> n
-  | NeverDischarge -> 0
-  | NotDeclare -> assert false
-
-let make_strength_0 () = 
-  let depth = Lib.sections_depth () in
-  let cwd = Lib.cwd() in
-  if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge
-
-let make_strength_1 () =
-  let depth = Lib.sections_depth () in
-  let cwd = Lib.cwd() in
-  if depth > 1 then DischargeAt (extract_dirpath_prefix 1 cwd, depth-1)
-  else NeverDischarge
-
-let make_strength_2 () =
-  let depth = Lib.sections_depth () in
-  let cwd = Lib.cwd() in
-  if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2)
-  else NeverDischarge
-
-let is_less_persistent_strength = function
-  | (NeverDischarge,_) -> false
-  | (NotDeclare,_) -> false
-  | (_,NeverDischarge) -> true
-  | (_,NotDeclare) -> true
-  | (DischargeAt (sp1,_),DischargeAt (sp2,_)) ->
-      is_dirpath_prefix_of sp1 sp2
-
 let strength_min (stre1,stre2) =
-  if is_less_persistent_strength (stre1,stre2) then stre1 else stre2
+  if stre1 = Local or stre2 = Local then Local else Global
+
+let string_of_strength = function
+  | Local -> "(local)"
+  | Global -> "(global)"
+
+(* XML output hooks *)
+let xml_declare_variable = ref (fun sp -> ())
+let xml_declare_constant = ref (fun sp -> ())
+let xml_declare_inductive = ref (fun sp -> ())
+
+let if_xml f x = if !Options.xml_export then f x else ()
+
+let set_xml_declare_variable f = xml_declare_variable := if_xml f
+let set_xml_declare_constant f = xml_declare_constant := if_xml f
+let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
 (* Section variables. *)
 
@@ -78,14 +64,13 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
-type variable_declaration = dir_path * section_variable_entry * strength
+type variable_declaration = dir_path * section_variable_entry * local_kind
 
 type checked_section_variable =
   | CheckedSectionLocalDef of constr * types * Univ.constraints * bool
   | CheckedSectionLocalAssum of types * Univ.constraints
 
-type checked_variable_declaration =
-    dir_path * checked_section_variable * strength
+type checked_variable_declaration = dir_path * checked_section_variable
 
 let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
 
@@ -95,7 +80,7 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.init_function = (fun () -> vartab := Idmap.empty);
 	    Summary.survive_section = false }
 
-let cache_variable ((sp,_),(id,(p,d,strength))) =
+let cache_variable ((sp,_),(id,(p,d,mk))) =
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -109,23 +94,35 @@ let cache_variable ((sp,_),(id,(p,d,strength))) =
         let (_,bd,ty) = Global.lookup_named id in
         CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  vartab := Idmap.add id (p,vd,strength) !vartab
+  vartab := Idmap.add id (p,vd) !vartab
 
 let (in_variable, out_variable) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     classify_function = (fun _ -> Dispose) }
 
-let declare_variable id obj =
-  let sp = add_leaf id (in_variable (id,obj)) in
+let declare_variable_common id obj =
+  let oname = add_leaf id (in_variable (id,obj)) in
   if is_implicit_args() then declare_var_implicits id;
-  sp
+  oname
+
+(* for initial declaration *)
+let declare_variable id obj =
+  let (_,kn as oname) = declare_variable_common id obj in
+  !xml_declare_variable kn;
+  Dischargedhypsmap.set_discharged_hyps (fst oname) [];
+  oname
+
+(* when coming from discharge: no xml output *)
+let redeclare_variable id discharged_hyps obj =
+  let oname = declare_variable_common id obj in
+  Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
 
 (* Globals: constants and parameters *)
 
-type constant_declaration = constant_entry * strength
+type constant_declaration = constant_entry * global_kind
 
-let csttab = ref (Spmap.empty : strength Spmap.t)
+let csttab = ref (Spmap.empty : global_kind Spmap.t)
 
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
@@ -133,7 +130,7 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.init_function = (fun () -> csttab := Spmap.empty);
 	    Summary.survive_section = false }
 
-let cache_constant ((sp,kn),(cdt,stre)) =
+let cache_constant ((sp,kn),(cdt,kind)) =
   (if Idmap.mem (basename sp) !vartab then
     errorlabstrm "cache_constant" 
       (pr_id (basename sp) ++ str " already exists"));
@@ -144,35 +141,26 @@ let cache_constant ((sp,kn),(cdt,stre)) =
   let kn' = Global.add_constant dir (basename sp) cdt in
     if kn' <> kn then
       anomaly "Kernel and Library names do not match";
-  (match stre with
-    | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
-        (* Only qualifications including the sections segment from the current
-           section to the discharge section is available for Remark & Fact *)
-        Nametab.push (Nametab.Until ((*n-Lib.sections_depth()+*)1)) sp (ConstRef kn)
-    | (NeverDischarge| DischargeAt _) -> 
-        (* All qualifications of Theorem, Lemma & Definition are visible *)
-        Nametab.push (Nametab.Until 1) sp (ConstRef kn)
-    | NotDeclare -> assert false);
-  csttab := Spmap.add sp stre !csttab
+  Nametab.push (Nametab.Until 1) sp (ConstRef kn);
+  csttab := Spmap.add sp kind !csttab
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn),(ce,stre)) =
+let load_constant i ((sp,kn),(_,kind)) =
   (if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
-  csttab := Spmap.add sp stre !csttab;
-  Nametab.push (Nametab.Until ((*depth_of_strength stre + *)i)) sp (ConstRef kn)
+  csttab := Spmap.add sp kind !csttab;
+  Nametab.push (Nametab.Until i) sp (ConstRef kn)
 
 (* Opening means making the name without its module qualification available *)
-let open_constant i ((sp,kn),(_,stre)) =
-  let n = depth_of_strength stre in
-  Nametab.push (Nametab.Exactly (i(*+n*))) sp (ConstRef kn)
+let open_constant i ((sp,kn),_) =
+  Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
 
-let dummy_constant (ce,stre) = dummy_constant_entry,stre
+let dummy_constant (ce,mk) = dummy_constant_entry,mk
 
 let export_constant cst = Some (dummy_constant cst)
 
@@ -195,15 +183,19 @@ let hcons_constant_declaration = function
          const_entry_opaque = ce.const_entry_opaque }, stre)
   | cd -> cd
 
-let declare_constant id (cd,stre) =
+let declare_constant id (cd,kind) =
   (* let cd = hcons_constant_declaration cd in *)
-  let oname = add_leaf id (in_constant (ConstantEntry cd,stre)) in
-  if is_implicit_args() then declare_constant_implicits (snd oname);
+  let (_,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in
+  if is_implicit_args() then declare_constant_implicits kn;
+  Dischargedhypsmap.set_discharged_hyps (fst oname) [] ;
+  !xml_declare_constant kn;
   oname
 
-let redeclare_constant id (cd,stre) =
-  let _,kn = add_leaf id (in_constant (GlobalRecipe cd,stre)) in
-  if is_implicit_args() then declare_constant_implicits kn
+(* when coming from discharge *)
+let redeclare_constant id discharged_hyps (cd,kind) =
+  let _,kn as oname = add_leaf id (in_constant (GlobalRecipe cd,kind)) in
+  if is_implicit_args() then declare_constant_implicits kn;
+  Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
 
 (* Inductives. *)
 
@@ -282,7 +274,7 @@ let (in_inductive, out_inductive) =
     subst_function = ident_subst_function;
     export_function = export_inductive } 
 
-let declare_mind mie =
+let declare_inductive_common mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives"
@@ -291,35 +283,46 @@ let declare_mind mie =
   if is_implicit_args() then declare_mib_implicits (snd oname);
   oname
 
+(* for initial declaration *)
+let declare_mind mie =
+  let (_,kn as oname) = declare_inductive_common mie in
+  Dischargedhypsmap.set_discharged_hyps (fst oname) [] ;
+  !xml_declare_inductive kn;
+  oname
+
+(* when coming from discharge: no xml output *)
+let redeclare_inductive discharged_hyps mie =
+ let oname = declare_inductive_common mie in
+ Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ;
+ oname
 
 (*s Test and access functions. *)
 
 let is_constant sp = 
   try let _ = Spmap.find sp !csttab in true with Not_found -> false
 
-let constant_strength sp = Spmap.find sp !csttab
+let constant_strength sp = Global
+let constant_kind sp = Spmap.find sp !csttab
 
 let get_variable id = 
-  let (p,x,str) = Idmap.find id !vartab in
-  let d = match x with
+  let (p,x) = Idmap.find id !vartab in
+  match x with
     | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
-    | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) in
-  (d,str)
+    | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty)
 
 let get_variable_with_constraints id = 
-  let (p,x,str) = Idmap.find id !vartab in
+  let (p,x) = Idmap.find id !vartab in
   match x with
-    | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst,str)
-    | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst,str)
+    | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst)
+    | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst)
 
-let variable_strength id =
-  let (_,_,str) = Idmap.find id !vartab in str
+let variable_strength _ = Local
 
 let find_section_variable id =
-  let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id
+  let (p,_) = Idmap.find id !vartab in Libnames.make_path p id
 
 let variable_opacity id =
-  let (_,x,_) = Idmap.find id !vartab in
+  let (_,x) = Idmap.find id !vartab in
   match x with
     | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq
     | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *)
@@ -369,7 +372,7 @@ let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
       try
-        let (p,_,_) = Idmap.find id !vartab in
+        let (p,_) = Idmap.find id !vartab in
         if dir=p then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
@@ -436,23 +439,21 @@ let is_global id =
   with Not_found -> 
     false
 
-let strength_of_global ref = match ref with 
-  | ConstRef kn -> constant_strength (sp_of_global None ref)
-  | VarRef id -> variable_strength id
-  | IndRef _ | ConstructRef _ -> NeverDischarge 
+let strength_of_global = function
+  | VarRef _ -> Local
+  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
 
 let library_part ref =
   let sp = Nametab.sp_of_global None ref in
   let dir,_ = repr_path sp in
   match strength_of_global ref with
-  | DischargeAt (dp,n) -> 
-      extract_dirpath_prefix n dp
-  | NeverDischarge ->
+  | Local -> 
+      anomaly "TODO";
+      extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+  | Global ->
       if is_dirpath_prefix_of dir (Lib.cwd ()) then
-	(* Theorem/Lemma not yet (fully) discharged *)
-	extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+        (* Not yet (fully) discharged *)
+        extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
       else
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
-  | NotDeclare -> assert false
-
diff --git a/library/declare.mli b/library/declare.mli
index c9d7cc574..3c04ddf57 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -19,6 +19,7 @@ open Indtypes
 open Safe_typing
 open Library
 open Nametab
+open Decl_kinds
 (*i*)
 
 (* This module provides the official functions to declare new variables, 
@@ -30,50 +31,59 @@ open Nametab
 
 open Nametab
 
+(* Declaration of local constructions (Variable/Hypothesis/Local) *)
+
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
-type variable_declaration = dir_path * section_variable_entry * strength
+type variable_declaration = dir_path * section_variable_entry * local_kind
 
 val declare_variable : variable -> variable_declaration -> object_name
 
-type constant_declaration = constant_entry * strength
+(* Declaration from Discharge *)
+val redeclare_variable :
+ variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit
+
+(* Declaration of global constructions *)
+(* i.e. Definition/Theorem/Axiom/Parameter/... *)
+
+type constant_declaration = constant_entry * global_kind
 
 (* [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration *)
 val declare_constant : identifier -> constant_declaration -> object_name
 
-val redeclare_constant : identifier -> Cooking.recipe * strength -> unit
-
-(*
-val declare_parameter : identifier -> constr -> constant
-*)
+val redeclare_constant :
+ identifier -> Dischargedhypsmap.discharged_hyps -> 
+      Cooking.recipe * global_kind -> unit
 
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block *)
 val declare_mind : mutual_inductive_entry -> object_name
 
+(* Declaration from Discharge *)
+val redeclare_inductive :
+ Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name
+
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
-val make_strength_0 : unit -> strength
-val make_strength_1 : unit -> strength
-val make_strength_2 : unit -> strength
-val is_less_persistent_strength : strength * strength -> bool
 val strength_min : strength * strength -> strength
+val string_of_strength : strength -> string
 
 (*s Corresponding test and access functions. *)
 
 val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
+val constant_kind : section_path -> global_kind
 
 val out_variable : Libobject.obj -> identifier * variable_declaration
-val get_variable : variable -> named_declaration * strength
+val get_variable : variable -> named_declaration
 val get_variable_with_constraints : 
-  variable -> named_declaration * Univ.constraints * strength
-val variable_strength : variable -> strength
+  variable -> named_declaration * Univ.constraints
+val variable_strength : variable -> strength 
 val find_section_variable : variable -> section_path
 val last_section_hyps : dir_path -> identifier list
 val clear_proofs : named_context -> named_context
@@ -108,3 +118,8 @@ val is_global : identifier -> bool
 val strength_of_global : global_reference -> strength
 
 val library_part : global_reference -> dir_path
+
+(* hooks for XML output *)
+val set_xml_declare_variable : (kernel_name -> unit) -> unit
+val set_xml_declare_constant : (kernel_name -> unit) -> unit
+val set_xml_declare_inductive : (kernel_name -> unit) -> unit
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
new file mode 100644
index 000000000..5241bf035
--- /dev/null
+++ b/library/dischargedhypsmap.ml
@@ -0,0 +1,59 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Libnames
+open Names
+open Term
+open Reduction
+open Declarations
+open Environ
+open Inductive
+open Libobject
+open Lib
+open Nametab
+
+type discharged_hyps = section_path list
+
+let discharged_hyps_map = ref Spmap.empty
+
+let cache_discharged_hyps_map (_,(sp,hyps)) = 
+  discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+
+let (in_discharged_hyps_map, _) =
+  declare_object { (default_object "DISCHARGED-HYPS-MAP") with
+    cache_function = cache_discharged_hyps_map;
+    load_function = (fun _ -> cache_discharged_hyps_map);
+    export_function = (fun x -> Some x) }
+
+let set_discharged_hyps sp hyps =
+ add_anonymous_leaf (in_discharged_hyps_map (sp,hyps))
+
+let get_discharged_hyps sp =
+  try
+   Spmap.find sp !discharged_hyps_map
+  with Not_found ->
+   anomaly ("No discharged hypothesis for object " ^ string_of_path sp)
+
+(*s Registration as global tables and rollback. *)
+
+let init () =
+  discharged_hyps_map := Spmap.empty
+
+let freeze () = !discharged_hyps_map
+
+let unfreeze dhm = discharged_hyps_map := dhm
+
+let _ = 
+  Summary.declare_summary "discharged_hypothesis"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_section = true }
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
new file mode 100644
index 000000000..cb3af4d47
--- /dev/null
+++ b/library/dischargedhypsmap.mli
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Libnames
+open Term
+open Environ
+open Nametab
+(*i*)
+
+type discharged_hyps = section_path list
+
+(*s Discharged hypothesis. Here we store the discharged hypothesis of each *)
+(*  constant or inductive type declaration.                                *)
+
+val set_discharged_hyps : section_path -> discharged_hyps -> unit
+val get_discharged_hyps : section_path -> discharged_hyps
diff --git a/library/lib.mli b/library/lib.mli
index 075be2890..56e79b661 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -119,6 +119,7 @@ val is_section_p : dir_path -> bool
 val start_compilation : dir_path -> module_path -> unit
 val end_compilation : dir_path -> object_prefix * library_segment
 
+(* The function [module_dp] returns the [dir_path] of the current module *)
 val module_dp : unit -> dir_path
 
 (*s Modules and module types *)
diff --git a/library/libnames.ml b/library/libnames.ml
index d5e9c8dc7..19e7d2833 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -205,8 +205,3 @@ type global_dir_reference =
       let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
           ModTypeRef kn'
 *)
-
-type strength = 
-  | NotDeclare
-  | DischargeAt of dir_path * int
-  | NeverDischarge
diff --git a/library/libnames.mli b/library/libnames.mli
index 915cdf3d2..04e552f4d 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -111,8 +111,3 @@ type global_dir_reference =
   | DirModule of object_prefix
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
-
-type strength = 
-  | NotDeclare
-  | DischargeAt of dir_path * int
-  | NeverDischarge