diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-27 17:27:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-27 17:27:31 +0000 |
commit | b84549caa97b373e5ccc5b6ad81592d0c2edb0bf (patch) | |
tree | 421ffd0d18753d2258fe76595d25974da2f957a8 /library | |
parent | 9c7027a1f668d4825a55b564c780651b2e7c8719 (diff) |
Ajout alias mutual_inductive_path = section_path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1282 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/declare.mli b/library/declare.mli index e561f222e..894cebd0d 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 |