diff options
| author | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
| commit | 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba (patch) | |
| tree | 5196448bc356711cd3924dc7f80e2908558d9238 /library | |
| parent | dd47dfc29f4b38dd2b1745ecbf452c3cd459b89b (diff) | |
Use ~strict argument consistently in push_context/push_context_set intfs
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
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 *) |