aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml4
-rw-r--r--stm/proofBlockDelimiter.ml2
-rw-r--r--stm/stm.ml26
-rw-r--r--stm/vernac_classifier.ml2
4 files changed, 18 insertions, 16 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index c8eb7b08f1..87d844edb3 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -138,7 +138,9 @@ module Make(T : Task) () = struct
set_slave_opt tl
(* We need to pass some options with one argument *)
| ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
- | "-require" | "-w" | "-color" | "-init-file"
+ | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from"
+ | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object"
+ | "-w" | "-color" | "-init-file"
| "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
| "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
x :: a :: set_slave_opt tl
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 6a78dd5529..2ff76e69f8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -50,7 +50,7 @@ let is_focused_goal_simple ~doc id =
| `Expired | `Error _ | `Valid None -> `Not
| `Valid (Some { Vernacstate.lemmas }) ->
Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
- let proof = Proof_global.get_proof proof in
+ let proof = Declare.Proof.get_proof 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
if List.for_all (fun x -> simple_goal sigma x rest) focused
diff --git a/stm/stm.ml b/stm/stm.ml
index 5b88ee3d68..f3768e9b99 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -27,7 +27,7 @@ open Feedback
open Vernacexpr
open Vernacextend
-module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"]
+module PG_compat = Vernacstate.Declare [@@ocaml.warning "-3"]
let is_vtkeep = function VtKeep _ -> true | _ -> false
let get_vtkeep = function VtKeep x -> x | _ -> assert false
@@ -147,7 +147,7 @@ let update_global_env () =
PG_compat.update_global_env ()
module Vcs_ = Vcs.Make(Stateid.Self)
-type future_proof = Proof_global.closed_proof_output Future.computation
+type future_proof = Declare.closed_proof_output Future.computation
type depth = int
type branch_type =
@@ -1164,7 +1164,7 @@ end = struct (* {{{ *)
let get_proof ~doc id =
match state_of_id ~doc id with
- | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas
+ | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
| _ -> None
let undo_vernac_classifier v ~doc =
@@ -1358,7 +1358,7 @@ module rec ProofTask : sig
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
+ t_assign : Declare.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1381,7 +1381,7 @@ module rec ProofTask : sig
?loc:Loc.t ->
drop_pt:bool ->
Stateid.t * Stateid.t -> Stateid.t ->
- Proof_global.closed_proof_output Future.computation
+ Declare.closed_proof_output Future.computation
(* If set, only tasks overlapping with this list are processed *)
val set_perspective : Stateid.t list -> unit
@@ -1397,7 +1397,7 @@ end = struct (* {{{ *)
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
+ t_assign : Declare.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1419,7 +1419,7 @@ end = struct (* {{{ *)
e_safe_states : Stateid.t list }
type response =
- | RespBuiltProof of Proof_global.closed_proof_output * float
+ | RespBuiltProof of Declare.closed_proof_output * float
| RespError of error
| RespStates of (Stateid.t * State.partial_state) list
@@ -1530,7 +1530,7 @@ end = struct (* {{{ *)
PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- let opaque = Proof_global.Opaque in
+ let opaque = Declare.Opaque in
stm_qed_delay_proof ~st ~id:stop
~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
ignore(Future.join checked_proof);
@@ -1664,7 +1664,7 @@ end = struct (* {{{ *)
let _proof = PG_compat.return_partial_proof () in
`OK_ADMITTED
else begin
- let opaque = Proof_global.Opaque in
+ let opaque = Declare.Opaque in
(* The original terminator, a hook, has not been saved in the .vio*)
let proof, _info =
@@ -1723,7 +1723,7 @@ end = struct (* {{{ *)
| `ERROR -> exit 1
| `ERROR_ADMITTED -> cst, false
| `OK_ADMITTED -> cst, false
- | `OK { Proof_global.name } ->
+ | `OK { Declare.name } ->
let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in
let c = Global.lookup_constant con in
let o = match c.Declarations.const_body with
@@ -2149,7 +2149,7 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).expr.CAst.loc in
let is_defined_expr = function
- | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
+ | VernacEndProof (Proved (Declare.Transparent,_)) -> true
| _ -> false in
let is_defined = function
| _, { expr = e } -> is_defined_expr e.CAst.v.expr
@@ -2310,7 +2310,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
Option.iter PG_compat.unfreeze lemmas;
PG_compat.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
- fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
+ fst (Proof.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
@@ -2514,7 +2514,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeep VtKeepAxiom ->
qed.fproof <- Some (None, ref false); None
| VtKeep opaque ->
- let opaque = let open Proof_global in match opaque with
+ let opaque = let open Declare in match opaque with
| VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
| VtKeepAxiom -> assert false
in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 567acb1c73..cf127648b4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification = function
| VtMeta -> "Meta "
| VtProofMode _ -> "Proof Mode"
-let vtkeep_of_opaque = let open Proof_global in function
+let vtkeep_of_opaque = let open Declare in function
| Opaque -> VtKeepOpaque
| Transparent -> VtKeepDefined
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:55:08 +0000