diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/library/declare.ml b/library/declare.ml index b0af8d5180..0764af4b06 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -172,17 +172,12 @@ let declare_constant_common id dhyps (cd,kind) = Notation.declare_ref_arguments_scope (ConstRef c); c -let declare_constant_gen internal id (cd,kind) = +let declare_constant ?(internal = UserVerbose) id (cd,kind) = let cd = hcons_constant_declaration cd in let kn = declare_constant_common id [] (ConstantEntry cd,kind) in !xml_declare_constant (internal,kn); kn -(* TODO: add a third function to distinguish between KernelVerbose - * and user Verbose *) -let declare_internal_constant = declare_constant_gen KernelSilent -let declare_constant = declare_constant_gen UserVerbose - (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = |