diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 37 |
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 |