Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 10 insertions, 27 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 968be059..938bfd06 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declare.mli,v 1.74.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declare.mli 7941 2006-01-28 23:07:59Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -36,42 +36,29 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
-type variable_declaration = dir_path * section_variable_entry * local_kind
+type variable_declaration = dir_path * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> object_name
 
-(* 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
+type constant_declaration = constant_entry * logical_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 declare_constant :
+ identifier -> constant_declaration -> constant
 
 val declare_internal_constant :
-  identifier -> constant_declaration -> object_name
-
-val redeclare_constant :
- identifier -> Dischargedhypsmap.discharged_hyps -> 
-      Cooking.recipe * global_kind -> unit
+  identifier -> constant_declaration -> constant
 
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : bool -> 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 strength_min : strength * strength -> strength
 val string_of_strength : strength -> string
 
@@ -79,24 +66,20 @@ val string_of_strength : strength -> string
 
 val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
-val constant_kind : section_path -> global_kind
+val constant_kind : section_path -> logical_kind
 
-val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable -> named_declaration
-val get_variable_with_constraints : 
-  variable -> named_declaration * Univ.constraints
 val variable_strength : variable -> strength 
-val variable_kind : variable -> local_kind
+val variable_kind : variable -> logical_kind
 val find_section_variable : variable -> section_path
 val last_section_hyps : dir_path -> identifier list
-val clear_proofs : named_context -> named_context
+val clear_proofs : named_context -> Environ.named_context_val
 
 (*s Global references *)
 
-val context_of_global_reference : global_reference -> section_context
 val strength_of_global : global_reference -> strength
 
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit