diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/library/declare.mli b/library/declare.mli index 1a9a0fac21..a8848660d7 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -21,23 +21,18 @@ type strength = | NeverDischarge type variable_declaration = constr * strength * bool - val declare_variable : identifier -> variable_declaration -> unit type constant_declaration = constant_entry * strength * bool - val declare_constant : identifier -> constant_declaration -> unit val declare_parameter : identifier -> constr -> unit - val declare_mind : mutual_inductive_entry -> unit - val declare_eliminations : section_path -> unit - val declare_syntax_constant : identifier -> constr -> unit val make_strength : string list -> strength |