diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 38 |
2 files changed, 16 insertions, 26 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 3d892fa5ca..f367167d48 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -51,8 +51,8 @@ let is_focused_goal_simple ~doc id = | `Valid (Some { Vernacstate.lemmas }) -> Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof -> let proof = Declare.Proof.get proof in - let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in - let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in + let Proof.{ goals=focused; stack=r1; sigma } = Proof.data proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ (Evd.shelf sigma) @ (Evar.Set.elements @@ Evd.given_up sigma) in if List.for_all (fun x -> simple_goal sigma x rest) focused then `Simple focused else `Not)) `Not lemmas diff --git a/stm/stm.ml b/stm/stm.ml index 3b7921f638..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 @@ -834,15 +830,11 @@ module State : sig (* to send states across worker/master *) val get_cached : Stateid.t -> Vernacstate.t - val same_env : Vernacstate.t -> Vernacstate.t -> bool - - type proof_part type partial_state = [ `Full of Vernacstate.t - | `ProofOnly of Stateid.t * proof_part ] + | `ProofOnly of Stateid.t * Vernacstate.Stm.pstate ] - val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -865,13 +857,9 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy - type proof_part = Vernacstate.Stm.pstate - type partial_state = [ `Full of Vernacstate.t - | `ProofOnly of Stateid.t * proof_part ] - - let proof_part_of_frozen st = Vernacstate.Stm.pstate st + | `ProofOnly of Stateid.t * Vernacstate.Stm.pstate ] let cache_state ~marshallable id = VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable)) @@ -924,7 +912,6 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = - let open Vernacstate in if VCS.get_state id <> EmptyState then () else try match what with | `Full s -> @@ -932,9 +919,11 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with lemmas = - PG_compat.copy_terminators - ~src:((get_cached prev).lemmas) ~tgt:s.lemmas } + then + let open Vernacstate in + { s with + lemmas = PG_compat.copy_terminators + ~src:((get_cached prev).lemmas) ~tgt:s.lemmas } else s with VCS.Expired -> s in VCS.set_state id (FullState s) @@ -953,8 +942,6 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env = Vernacstate.Stm.same_env - (* [define] puts the system in state [id] calling [f ()] *) (* [safe_id] is the last known valid state before execution *) let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true) @@ -1549,8 +1536,8 @@ end = struct (* {{{ *) match prev, this with | _, None -> None | Some (prev, o, `Cmd { cast = { expr }}), Some n - when is_tac expr && State.same_env o n -> (* A pure tactic *) - Some (id, `ProofOnly (prev, State.proof_part_of_frozen n)) + when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *) + Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n)) | Some _, Some s -> if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) @@ -1931,7 +1918,8 @@ end = struct (* {{{ *) str" solves the goal and leaves no unresolved existential variables. The following" ++ str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) end) () - with e when CErrors.noncritical e -> RespError (CErrors.print e) + with e when CErrors.noncritical e -> + RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int (fst r_ast) ++ str ")") let name_of_task { t_name } = t_name let name_of_request { r_name } = r_name @@ -2344,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 = |