diff options
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | library/declare.mli | 10 |
3 files changed, 7 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 4152ec39e2..fa95bc2034 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -366,6 +366,7 @@ type variable_path = section_path type constant_path = section_path type inductive_path = section_path * int type constructor_path = inductive_path * int +type mutual_inductive_path = section_path (* Hash-consing of identifier *) module Hident = Hashcons.Make( diff --git a/kernel/names.mli b/kernel/names.mli index 770bfe5040..bd3d0e590c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -113,6 +113,7 @@ type variable_path = section_path type constant_path = section_path type inductive_path = section_path * int type constructor_path = inductive_path * int +type mutual_inductive_path = section_path (* Hash-consing *) val hcons_names : unit -> diff --git a/library/declare.mli b/library/declare.mli index e561f222e0..894cebd0d9 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -49,11 +49,11 @@ val declare_parameter : identifier -> constr -> constant_path (* [declare_constant id cd] 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 -> section_path +val declare_mind : mutual_inductive_entry -> mutual_inductive_path (* [declare_eliminations sp] declares elimination schemes associated to the mutual inductive block refered by [sp] *) -val declare_eliminations : section_path -> unit +val declare_eliminations : mutual_inductive_path -> unit val out_inductive : Libobject.obj -> mutual_inductive_entry @@ -71,7 +71,7 @@ val constant_or_parameter_strength : constant_path -> strength val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable_path -> named_declaration * strength * sticky val variable_strength : variable_path -> strength -val find_section_variable : identifier -> section_path +val find_section_variable : identifier -> variable_path (*s [global_reference k id] returns the object corresponding to the name [id] in the global environment. It may be a constant, @@ -98,8 +98,8 @@ val construct_reference : Environ.env -> path_kind -> identifier -> constr val is_global : identifier -> bool -val path_of_inductive_path : inductive_path -> section_path -val path_of_constructor_path : constructor_path -> section_path +val path_of_inductive_path : inductive_path -> mutual_inductive_path +val path_of_constructor_path : constructor_path -> mutual_inductive_path (* Look up function for the default elimination constant *) val elimination_suffix : sorts -> string |