diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 6 | ||||
| -rw-r--r-- | library/nametab.ml | 9 |
3 files changed, 9 insertions, 8 deletions
diff --git a/library/global.ml b/library/global.ml index ce37dfecff..ed847b7cdb 100644 --- a/library/global.ml +++ b/library/global.ml @@ -81,7 +81,7 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index 324181e79e..03bc945dad 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,11 +32,11 @@ val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * Entries.section_def_entry) -> unit val export_private_constants : in_section:bool -> - Safe_typing.private_constants Entries.constant_entry -> - unit Entries.constant_entry * Safe_typing.exported_private_constant list + Safe_typing.private_constants Entries.definition_entry -> + unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t diff --git a/library/nametab.ml b/library/nametab.ml index 84225f8639..08881d6d7a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -81,8 +81,9 @@ struct Module F (X : S). Module X. The argument X of the functor F is masked by the inner module X. *) - let masking_absolute n = - Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + let warn_masking_absolute = + CWarnings.create ~name:"masking-absolute-name" ~category:"deprecated" + (fun n -> str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) type user_name = U.t @@ -121,7 +122,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -154,7 +155,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in |