diff options
| author | vsiles | 2010-09-02 16:38:36 +0000 |
|---|---|---|
| committer | vsiles | 2010-09-02 16:38:36 +0000 |
| commit | 93383861409291653f393f949e12e5604951dadc (patch) | |
| tree | 0ebdc0c6d1e53effce0ae2d86735b6d20189d69c /library | |
| parent | 51b0246d286fba37019af058fc484369bcabf7f9 (diff) | |
* removed declare_constant and declare_internal_constant
(declare_constant_gen was not exported, leading to a lot of silly tests
before calling those functions) and replaced them by
declare_constant : ?internal:internal_flat -> ...
declare_constant's default behaviour is the same as the old declare_constant.
* fixed the default behaviour of inductive scheme failure during coq's
compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 7 | ||||
| -rw-r--r-- | library/declare.mli | 12 |
2 files changed, 8 insertions, 11 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 = diff --git a/library/declare.mli b/library/declare.mli index b6ed0a815d..1ad733816f 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -43,17 +43,19 @@ type constant_declaration = constant_entry * logical_kind (** [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 *) + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent + + *) type internal_flag = | KernelVerbose | KernelSilent | UserVerbose val declare_constant : - identifier -> constant_declaration -> constant - -val declare_internal_constant : - identifier -> constant_declaration -> constant + ?internal:internal_flag -> identifier -> constant_declaration -> constant (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of |