aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/modintern.ml2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli1
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli1
-rw-r--r--library/universes.ml2
-rw-r--r--pretyping/evd.ml16
-rw-r--r--pretyping/evd.mli2
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--stm/lemmas.ml2
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/vernacentries.ml12
13 files changed, 41 insertions, 14 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml
index bf0b2f980..35e731137 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,7 +62,7 @@ let transl_with_decl env = function
WithMod (fqid,lookup_module qid)
| CWith_Definition ((_,fqid),c) ->
let c, ectx = interp_constr env (Evd.from_env env) c in
- let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in
+ let ctx = Evd.evar_context_universe_context ectx in
WithDef (fqid,(c,ctx))
let loc_of_module = function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d6bd75478..d9adca0c9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -246,6 +246,8 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
else add_constraints (Now (Future.join fc)) e)
{e with future_cst = []} e.future_cst
+let is_joined_environment e = List.is_empty e.future_cst
+
(** {6 Various checks } *)
let exists_modlabel l senv = Label.Set.mem l senv.modlabels
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index abd5cd7ae..a57fb108c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -51,6 +51,7 @@ val is_curmod_library : safe_environment -> bool
val join_safe_environment :
?except:Future.UUIDSet.t -> safe_environment -> safe_environment
+val is_joined_environment : safe_environment -> bool
(** {6 Enriching a safe environment } *)
(** Insertion of local declarations (Local or Variables) *)
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
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 18e668d28..fe96aa347 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -330,9 +330,23 @@ let union_evar_universe_context ctx ctx' =
type 'a in_evar_universe_context = 'a * evar_universe_context
-let evar_universe_context_set ctx = ctx.uctx_local
+let evar_universe_context_set diff ctx =
+ let initctx = ctx.uctx_local in
+ let cstrs =
+ Univ.LSet.fold
+ (fun l cstrs ->
+ try
+ match Univ.LMap.find l ctx.uctx_univ_variables with
+ | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+ | None -> cstrs
+ with Not_found -> cstrs)
+ (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
+ in
+ Univ.ContextSet.add_constraints cstrs initctx
+
let evar_universe_context_constraints ctx = snd ctx.uctx_local
let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
+
let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
let evar_universe_context_subst ctx = ctx.uctx_univ_variables
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 15ce979d0..f2d8a8335 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -475,7 +475,7 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * evar_universe_context
-val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set
val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
val evar_context_universe_context : evar_universe_context -> Univ.universe_context
val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5bff3c813..8be96285f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -292,7 +292,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
let body = c and typ = nf t in
let used_univs_body = Universes.universes_of_constr body in
let used_univs_typ = Universes.universes_of_constr typ in
- let ctx = Evd.evar_universe_context_set universes in
+ let ctx = Evd.evar_universe_context_set Univ.UContext.empty universes in
if keep_body_ucst_sepatate then
(* For vi2vo compilation proofs are computed now but we need to
* complement the univ constraints of the typ with the ones of
@@ -317,7 +317,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
let initunivs = Evd.evar_context_universe_context universes in
Future.from_val (initunivs, nf t),
Future.chain ~pure:true p (fun (pt,eff) ->
- (pt, Evd.evar_universe_context_set (Future.force univs)), eff)
+ (pt, Evd.evar_universe_context_set initunivs (Future.force univs)), eff)
in
let entries =
Future.map2 (fun p (_, t) ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6cece32e0..5eebd0d9d 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -436,7 +436,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = Evd.evar_universe_context_set ctx in
+ let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 177be2c20..e4240cb5c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -268,7 +268,7 @@ let add_rewrite_hint bases ort t lcsr =
let c, ctx = Constrintern.interp_constr env sigma ce in
let ctx =
if poly then
- Evd.evar_universe_context_set ctx
+ Evd.evar_universe_context_set Univ.UContext.empty ctx
else
let cstrs = Evd.evar_universe_context_constraints ctx in
(Global.add_constraints cstrs; Univ.ContextSet.empty)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7cf0477f9..1b396d57b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1064,7 +1064,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
- let ctx = Evd.evar_universe_context_set ctx in
+ let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
let ctx = Universes.restrict_universe_context ctx vars in
let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
let ctx = Univ.ContextSet.to_context ctx in
@@ -1097,7 +1097,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
- let ctx = Evd.evar_universe_context_set ctx in
+ let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
let ctx = Univ.ContextSet.to_context ctx in
ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx)
fixnames fixdecls fixtypes fiximps);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 849b1d47d..61ebc9bbe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1563,7 +1563,7 @@ let vernac_global_check c =
let sigma = Evd.from_env env in
let c,ctx = interp_constr env sigma c in
let senv = Global.safe_env() in
- let cstrs = snd (Evd.evar_universe_context_set ctx) in
+ let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in
let senv = Safe_typing.add_constraints cstrs senv in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
@@ -1628,9 +1628,13 @@ let vernac_print = function
msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
| PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
| PrintUniverses (b, None) ->
- let univ = Global.universes () in
- let univ = if b then Univ.sort_universes univ else univ in
- msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ)
+ let univ = Global.universes () in
+ let univ = if b then Univ.sort_universes univ else univ in
+ let pr_remaining =
+ if Global.is_joined_environment () then mt ()
+ else str"There may remain asynchronous universe constraints"
+ in
+ msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
| PrintUniverses (b, Some s) -> dump_universes b s
| PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
| PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 20:26:13 +0000