aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh9
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli3
-rw-r--r--engine/proofview.ml4
-rw-r--r--engine/proofview.mli4
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli2
-rw-r--r--proofs/proof.ml4
-rw-r--r--proofs/proof.mli4
-rw-r--r--stm/stm.ml8
-rw-r--r--vernac/declare.ml8
-rw-r--r--vernac/declare.mli8
-rw-r--r--vernac/vernacinterp.ml7
-rw-r--r--vernac/vernacstate.ml6
-rw-r--r--vernac/vernacstate.mli3
15 files changed, 45 insertions, 33 deletions
diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
new file mode 100644
index 0000000000..f0878202d3
--- /dev/null
+++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then
+
+ elpi_CI_REF=update-s-univs
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+ equations_CI_REF=update-s-univs
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
diff --git a/engine/evd.ml b/engine/evd.ml
index 555c3a150c..b20700143f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1160,8 +1160,8 @@ let universe_binders evd = UState.universe_binders evd.universes
let universes evd = UState.ugraph evd.universes
-let update_sigma_env evd env =
- { evd with universes = UState.update_sigma_env evd.universes env }
+let update_sigma_univs ugraph evd =
+ { evd with universes = UState.update_sigma_univs evd.universes ugraph }
exception UniversesDiffer = UState.UniversesDiffer
diff --git a/engine/evd.mli b/engine/evd.mli
index 5c7a529b9c..9dc106a3d7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -660,7 +660,8 @@ val fix_undefined_variables : evar_map -> evar_map
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
-val update_sigma_env : evar_map -> env -> evar_map
+(** Lift [UState.update_sigma_univs] *)
+val update_sigma_univs : UGraph.t -> evar_map -> evar_map
(** Polymorphic universes *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2fc5ade0d2..5b0e6f5785 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1037,8 +1037,8 @@ module Unsafe = struct
let mark_as_unresolvables p evs =
{ p with solution = mark_in_evm ~goal:false p.solution evs }
- let update_sigma_env pv env =
- { pv with solution = Evd.update_sigma_env pv.solution env }
+ let update_sigma_univs ugraph pv =
+ { pv with solution = Evd.update_sigma_univs ugraph pv.solution }
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8853013a84..db6509c84e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -500,8 +500,8 @@ module Unsafe : sig
val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
Proofview_monad.goal_with_state list
- (** [update_sigma_env] lifts [Evd.update_sigma_env] to the proofview *)
- val update_sigma_env : proofview -> Environ.env -> proofview
+ (** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proofview *)
+ val update_sigma_univs : UGraph.t -> proofview -> proofview
end
diff --git a/engine/uState.ml b/engine/uState.ml
index ca0a21acf7..8d1584cd95 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -568,8 +568,8 @@ let emit_side_effects eff u =
let u = demote_seff_univs (fst uctx) u in
merge_seff u uctx
-let update_sigma_env uctx env =
- let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in
+let update_sigma_univs uctx ugraph =
+ let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) ugraph in
let eunivs =
{ uctx with
initial_universes = univs;
diff --git a/engine/uState.mli b/engine/uState.mli
index 607c6c9452..7fec03e3b2 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -185,7 +185,7 @@ val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
(** {5 TODO: Document me} *)
-val update_sigma_env : t -> Environ.env -> t
+val update_sigma_univs : t -> UGraph.t -> t
(** {5 Pretty-printing} *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index d7904c56a8..616cbf9678 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -353,8 +353,8 @@ let compact p =
let entry, proofview = Proofview.compact p.entry p.proofview in
{ p with proofview; entry }
-let update_sigma_env p env =
- let proofview = Proofview.Unsafe.update_sigma_env p.proofview env in
+let update_sigma_univs ugraph p =
+ let proofview = Proofview.Unsafe.update_sigma_univs ugraph p.proofview in
{ p with proofview }
(*** Function manipulation proof extra informations ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index a0d4759bfc..ffb8380147 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -76,8 +76,8 @@ val partial_proof : t -> EConstr.constr list
val compact : t -> t
-(** [update_sigma_env] lifts [Evd.update_sigma_env] to the proof *)
-val update_sigma_env : t -> Environ.env -> t
+(** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proof *)
+val update_sigma_univs : UGraph.t -> t -> t
(* Returns the proofs (with their type) of the initial goals.
Raises [UnfinishedProof] is some goals remain to be considered.
diff --git a/stm/stm.ml b/stm/stm.ml
index 9999e66c45..4ca0c365bf 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -142,10 +142,6 @@ let may_pierce_opaque = function
| VernacExtend (("ExtractionInductive",_), _) -> true
| _ -> false
-let update_global_env () =
- if PG_compat.there_are_pending_proofs () then
- PG_compat.update_global_env ()
-
module Vcs_ = Vcs.Make(Stateid.Self)
type future_proof = Declare.Proof.closed_proof_output Future.computation
@@ -2336,7 +2332,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
let inject_non_pstate (s,l) =
- Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
+ Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l;
+ if PG_compat.there_are_pending_proofs () then
+ PG_compat.update_sigma_univs (Global.universes ())
in
let rec pure_cherry_pick_non_pstate safe_id id =
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 52be6f7946..12d6cb9f49 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1734,8 +1734,8 @@ let return_proof ps =
let p, uctx = prepare_proof ~unsafe_typ:false ps in
List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
-let update_global_env =
- map ~f:(fun p -> Proof.update_sigma_env p (Global.env ()))
+let update_sigma_univs ugraph p =
+ map ~f:(Proof.update_sigma_univs ugraph) p
let next = let n = ref 0 in fun () -> incr n; !n
@@ -2251,7 +2251,7 @@ let rec solve_obligation prg num tac =
let scope = Locality.Global Locality.ImportNeedQualified in
let kind = kind_of_obligation (snd obl.obl_status) in
let evd = Evd.from_ctx (Internal.get_uctx prg) in
- let evd = Evd.update_sigma_env evd (Global.env ()) in
+ let evd = Evd.update_sigma_univs (Global.universes ()) evd in
let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in
let proof_ending =
let name = Internal.get_name prg in
@@ -2292,7 +2292,7 @@ and solve_obligation_by_tac prg obls i tac =
| None -> !default_tactic
in
let uctx = Internal.get_uctx prg in
- let uctx = UState.update_sigma_env uctx (Global.env ()) in
+ let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
let poly = Internal.get_poly prg in
match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
| None -> None
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 3001d0d206..1ad79928d5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -246,10 +246,10 @@ module Proof : sig
val compact : t -> t
- (** Update the proofs global environment after a side-effecting command
- (e.g. a sublemma definition) has been run inside it. Assumes
- there_are_pending_proofs. *)
- val update_global_env : t -> t
+ (** Update the proof's universe information typically after a
+ side-effecting command (e.g. a sublemma definition) has been run
+ inside it. *)
+ val update_sigma_univs : UGraph.t -> t -> t
val get_open_goals : t -> int
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 6be2fb0d43..edf48fef1a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -211,8 +211,11 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
(fun ~st ->
let before_univs = Global.universes () in
let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
- if before_univs == Global.universes () then pstack, pm
- else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm)
+ let after_univs = Global.universes () in
+ if before_univs == after_univs then pstack, pm
+ else
+ let f = Declare.Proof.update_sigma_univs after_univs in
+ Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm)
~st
(* XXX: This won't properly set the proof mode, as of today, it is
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 6d12d72408..204008997d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -80,7 +80,7 @@ module LemmaStack = struct
type t = Declare.Proof.t * Declare.Proof.t list
- let map f (pf, pfl) = (f pf, List.map f pfl)
+ let map ~f (pf, pfl) = (f pf, List.map f pfl)
let map_top ~f (pf, pfl) = (f pf, pfl)
let pop (ps, p) = match p with
@@ -96,7 +96,7 @@ module LemmaStack = struct
let get_all_proof_names (pf : t) =
let prj x = Declare.Proof.get x in
- let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
+ let (pn, pns) = map ~f:Proof.(function pf -> (data (prj pf)).name) pf in
pn :: pns
let copy_info src tgt =
@@ -218,7 +218,7 @@ module Declare_ = struct
Declare.Proof.info pt)
let discard_all () = s_lemmas := None
- let update_global_env () = dd (Declare.Proof.update_global_env)
+ let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)
let get_current_context () = cc Declare.Proof.get_current_context
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 5efdb3cc68..e1b13dcb73 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -40,6 +40,7 @@ module LemmaStack : sig
val pop : t -> Declare.Proof.t * t option
val push : t option -> Declare.Proof.t -> t
+ val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a
@@ -112,7 +113,7 @@ module Declare : sig
val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
val discard_all : unit -> unit
- val update_global_env : unit -> unit
+ val update_sigma_univs : UGraph.t -> unit
val get_current_context : unit -> Evd.evar_map * Environ.env
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:28:09 +0000