diff options
| author | Pierre-Marie Pédrot | 2015-06-01 11:40:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-06-01 11:40:35 +0200 |
| commit | dc2405f017f5b784d3c7393ae2b4ba1ef710d10b (patch) | |
| tree | ea2defb1691834c73f35bb9cf8912cdb04f3f7b8 /library | |
| parent | 3fcadca93b8d9dd70d9d93412cbacf8d4e851ed7 (diff) | |
| parent | 43aa642ad4f2d30029c1c1f272ba162b6801a40b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 1 | ||||
| -rw-r--r-- | library/universes.ml | 2 |
3 files changed, 7 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index 875097e48c..49fa2ef28f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -19,6 +19,7 @@ module GlobalSafeEnv : sig val safe_env : unit -> Safe_typing.safe_environment val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit + val is_joined_environment : unit -> bool end = struct @@ -27,6 +28,9 @@ let global_env = ref Safe_typing.empty_environment let join_safe_environment ?except () = global_env := Safe_typing.join_safe_environment ?except !global_env +let is_joined_environment () = + Safe_typing.is_joined_environment !global_env + let () = Summary.declare_summary global_env_summary_name { Summary.freeze_function = (function @@ -50,6 +54,7 @@ end let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () +let is_joined_environment = GlobalSafeEnv.is_joined_environment let env () = Safe_typing.env_of_safe_env (safe_env ()) diff --git a/library/global.mli b/library/global.mli index 62d7ea3210..248e1f86dd 100644 --- a/library/global.mli +++ b/library/global.mli @@ -112,6 +112,7 @@ val import : val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit +val is_joined_environment : unit -> bool val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool diff --git a/library/universes.ml b/library/universes.ml index 3a8ee26254..3a7a769075 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -845,7 +845,7 @@ let normalize_context_set ctx us algs = Constraint.add (canon, Univ.Eq, g) cst) global cstrs in - let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in + let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) (ctx, LMap.empty, Constraint.empty) partition |