diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/library/declare.mli b/library/declare.mli index 07b9d98b6..273a2b344 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -10,9 +10,11 @@ (*i*) open Names +open Libnames open Term open Sign open Declarations +open Entries open Indtypes open Safe_typing open Library @@ -34,16 +36,16 @@ type section_variable_entry = type variable_declaration = dir_path * section_variable_entry * strength -val declare_variable : variable -> variable_declaration -> section_path +val declare_variable : variable -> variable_declaration -> object_name -type constant_declaration = global_declaration * strength +type constant_declaration = constant_entry * strength (* [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 -> constant +val declare_constant : identifier -> constant_declaration -> object_name -val redeclare_constant : constant -> Cooking.recipe * strength -> unit +val redeclare_constant : identifier -> Cooking.recipe * strength -> unit (* val declare_parameter : identifier -> constr -> constant @@ -52,7 +54,7 @@ val declare_parameter : identifier -> constr -> 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 *) -val declare_mind : mutual_inductive_entry -> mutual_inductive +val declare_mind : mutual_inductive_entry -> object_name val out_inductive : Libobject.obj -> mutual_inductive_entry @@ -65,7 +67,7 @@ val strength_min : strength * strength -> strength (*s Corresponding test and access functions. *) val is_constant : section_path -> bool -val constant_strength : constant -> strength +val constant_strength : section_path -> strength val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable -> named_declaration * strength @@ -86,11 +88,11 @@ val constr_of_reference : global_reference -> constr raise [Not_found] if not a global *) val reference_of_constr : constr -> global_reference -val global_qualified_reference : Nametab.qualid -> constr +val global_qualified_reference : qualid -> constr val global_absolute_reference : section_path -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -val construct_qualified_reference : Nametab.qualid -> constr +val construct_qualified_reference : qualid -> constr val construct_absolute_reference : section_path -> constr (* This should eventually disappear *) @@ -98,7 +100,7 @@ val construct_absolute_reference : section_path -> constr the name [id] in the global environment. It looks also for variables in a given environment instead of looking in the current global environment. *) val global_reference : identifier -> constr -val construct_reference : Environ.env -> identifier -> constr +val construct_reference : Sign.named_context option -> identifier -> constr val is_global : identifier -> bool |