diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:56:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:56:08 +0100 |
| commit | 333b2f369c9a0ab61597cc9174a77632d263f386 (patch) | |
| tree | 2e2db1d45b26c1a758346959a83cd6cd84c36e6a /library | |
| parent | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (diff) | |
| parent | 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba (diff) | |
Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/library/global.ml b/library/global.ml index d4262683bb..fbbe09301b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,7 +90,7 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) let push_section_context c = globalize0 (Safe_typing.push_section_context c) 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_set ~strict c = globalize0 (Safe_typing.push_context_set ~strict c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) @@ -206,7 +206,7 @@ let current_dirpath () = let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in - push_context_set false ctx; a + push_context_set ~strict:true ctx; a let register_inline c = globalize0 (Safe_typing.register_inline c) let register_inductive c r = globalize0 (Safe_typing.register_inductive c r) diff --git a/library/global.mli b/library/global.mli index db0f87df7e..a38fde41a5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -60,7 +60,7 @@ val add_mind : (** Extra universe constraints *) val add_constraints : Univ.Constraint.t -> unit -val push_context_set : bool -> Univ.ContextSet.t -> unit +val push_context_set : strict:bool -> Univ.ContextSet.t -> unit (** Non-interactive modules and module types *) |