diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-05-27 11:43:11 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-05-27 11:43:11 +0200 |
commit | 866c41b9720413e00194ba7addb9c4277e114890 (patch) | |
tree | 37fe660b28acfbaa6f3f304b6b9f3eebcf15dddb /library | |
parent | ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (diff) |
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.
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 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 |