diff options
| author | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
| commit | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (patch) | |
| tree | 7546ab8a3bf1a0e2b5a75028e9efcade1d8d4321 /library/declare.ml | |
| parent | 13716dc6561a3379ba130f07ce7ecd1df379475c (diff) | |
Hopefully better names to constructors of internal_flag, as discussed
with Enrico.
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/declare.ml b/library/declare.ml index c3181e4c75..8438380c9c 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 = |