diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 22:26:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 22:26:14 +0000 |
| commit | 161e0e8073e84ab0f3e982baf7f7122dd3ddfb85 (patch) | |
| tree | 83ef95a0f573d7777aa92221c00b662f199000ad /library/declare.mli | |
| parent | 8b744c66b48182406ecc6d671312204c74c1a53f (diff) | |
Prise en compte des noms longs dans les Hints et les Coercions, et réorganisations diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/library/declare.mli b/library/declare.mli index 927f05fde..e561f222e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -29,7 +29,7 @@ type sticky = bool type variable_declaration = section_variable_entry * strength * sticky -val declare_variable : identifier -> variable_declaration -> unit +val declare_variable : identifier -> variable_declaration -> variable_path type constant_declaration_type = | ConstantEntry of constant_entry @@ -39,10 +39,16 @@ type opacity = bool type constant_declaration = constant_declaration_type * strength * opacity -val declare_constant : identifier -> constant_declaration -> unit +(* [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_path -val declare_parameter : identifier -> constr -> unit +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 (* [declare_eliminations sp] declares elimination schemes associated |