From 866c41b9720413e00194ba7addb9c4277e114890 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 27 May 2015 11:43:11 +0200 Subject: Fix bug #4159 Some asynchronous constraints between initial universes and the ones at the end of a proof were forgotten. Also add a message to print universes indicating if all the constraints are processed already or not. --- library/global.ml | 5 +++++ library/global.mli | 1 + library/universes.ml | 2 +- 3 files changed, 7 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 875097e48..49fa2ef28 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 62d7ea321..248e1f86d 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 3a8ee2625..3a7a76907 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 -- cgit v1.2.3