diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-23 18:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-23 18:25:15 +0200 |
| commit | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (patch) | |
| tree | 7546ab8a3bf1a0e2b5a75028e9efcade1d8d4321 /library | |
| parent | 13716dc6561a3379ba130f07ce7ecd1df379475c (diff) | |
Hopefully better names to constructors of internal_flag, as discussed
with Enrico.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 10 | ||||
| -rw-r--r-- | library/declare.mli | 6 |
2 files changed, 8 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml index c3181e4c7..8438380c9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -28,9 +28,9 @@ open Decl_kinds (** flag for internal message display *) type internal_flag = - | KernelVerbose (* kernel action, a message is displayed *) - | KernelSilent (* kernel action, no message is displayed *) - | UserVerbose (* user action, a message is displayed *) + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) (** Declaration of section variables and local definitions *) @@ -253,7 +253,7 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -283,7 +283,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff let kn = declare_constant_common id cst in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = diff --git a/library/declare.mli b/library/declare.mli index d8a00db0c..76538a624 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -43,9 +43,9 @@ type constant_declaration = constant_entry * logical_kind *) type internal_flag = - | KernelVerbose - | KernelSilent - | UserVerbose + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> |