aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli7
-rw-r--r--ltac/extratactics.ml44
-rw-r--r--ltac/g_ltac.ml43
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--stm/stm.ml213
-rw-r--r--stm/stm.mli83
-rw-r--r--stm/vernac_classifier.ml13
7 files changed, 275 insertions, 50 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc..6ce15a7c5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -454,7 +454,7 @@ type vernac_type =
| VtStartProof of vernac_start
| VtSideff of vernac_sideff_type
| VtQed of vernac_qed_type
- | VtProofStep of bool (* parallelize *)
+ | VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * report_with
| VtStm of vernac_control * vernac_part_of_script
@@ -476,6 +476,11 @@ and vernac_control =
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and proof_step = { (* TODO: inline with OCaml 4.03 *)
+ parallel : bool;
+ proof_block_detection : proof_block_name option
+}
+and proof_block_name = string (* open type of delimiters *)
type vernac_when =
| VtNow
| VtLater
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 5d3c149ab..57fad8511 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -872,7 +872,7 @@ END;;
mode. *)
VERNAC COMMAND EXTEND GrabEvars
[ "Grab" "Existential" "Variables" ]
- => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+ => [ Vernac_classifier.classify_as_proofstep ]
-> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ]
END
@@ -903,7 +903,7 @@ END
(* Command to add every unshelved variables to the focus *)
VERNAC COMMAND EXTEND Unshelve
[ "Unshelve" ]
- => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+ => [ Vernac_classifier.classify_as_proofstep ]
-> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ]
END
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 3579fc10f..c8287a2c8 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,8 @@ VERNAC tactic_mode EXTEND VernacSolve
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
- [ VtProofStep true, VtLater ] -> [
+ [ VtProofStep{ parallel = true; proof_block_detection = None },
+ VtLater ] -> [
vernac_solve SelectAll n t def
]
END
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143d..4c3bebd65 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -98,7 +98,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
let classify_proof_instr = function
| { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
- | _ -> VtProofStep false, VtLater
+ | _ -> Vernac_classifier.classify_as_proofstep
(* We use the VERNAC EXTEND facility with a custom non-terminal
to populate [proof_mode] with a new toplevel interpreter.
diff --git a/stm/stm.ml b/stm/stm.ml
index 492ac99fe..35f7295dd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -171,7 +171,7 @@ type branch_type =
| `Edit of
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
- ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
+ ctac : bool; (* is a tactic *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : aast;
cids : Id.t list;
@@ -229,17 +229,22 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
let default_info () =
{ n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+module DynBlockData : Dyn.S = Dyn.Make(struct end)
+
(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
* no constraint on properties, here we impose boxes to be non overlapping. *)
type box =
| ProofTask of pt
- | ErrorBound of eb
+ | ErrorBound of static_block_declaration * proof_block_name
and pt = { (* TODO: inline records in OCaml 4.03 *)
- start : Stateid.t;
+ lemma : Stateid.t;
qed : Stateid.t;
}
-and eb = {
- stuff : unit;
+and static_block_declaration = {
+ start : Stateid.t;
+ stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
}
(* Functions that work on a Vcs with a specific branch type *)
@@ -346,9 +351,9 @@ module VCS : sig
val nodes_in_slice : start:id -> stop:id -> Stateid.t list
val create_proof_task_box : id list -> qed:id -> start:id -> unit
- val create_error_bound_box : id list -> switch:id -> unit
+ val create_error_bound_box : static_block_declaration -> string -> unit
val box_of : id -> box list
- val delete_proof_task_box_of : id -> unit
+ val delete_boxes_of : id -> unit
val proof_task_box_of : id -> pt option
val proof_nesting : unit -> int
@@ -465,7 +470,12 @@ end = struct (* {{{ *)
nodefmt oc id
end)
(Dag.Property.having_it b);
- fprintf oc "color=blue; }\n" in
+ match Dag.Property.data b with
+ | ErrorBound ({ dynamic_switch = id }, lbl) ->
+ fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id);
+ fprintf oc "color=red; }\n"
+ | ProofTask _ -> fprintf oc "color=blue; }\n"
+ in
List.iter rec_print (outerboxes !boxes);
Stateid.Set.iter (nodefmt oc) !ids;
@@ -576,6 +586,17 @@ end = struct (* {{{ *)
{ (get_info id) with state = Empty; vcs_backup = None,None } in
let copy_info_w_state v id =
Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+ let copy_error_bound_boxes v =
+ let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
+ let props =
+ Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
+ let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
+ (* XXX check if par: works here, since we copy a single node *)
+ List.fold_left (fun v p ->
+ Vcs_.create_property v
+ (Stateid.Set.elements (Vcs_.Dag.Property.having_it p))
+ (Vcs_.Dag.Property.data p)) v props
+ in
let v = Vcs_.empty start in
let v = copy_info v start in
let v = List.fold_right (fun (id,tr) v ->
@@ -592,7 +613,8 @@ end = struct (* {{{ *)
let v = fill stop in
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
- copy_info_w_state v start
+ let v = copy_info_w_state v start in
+ copy_error_bound_boxes v
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -606,18 +628,16 @@ end = struct (* {{{ *)
List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets)
l
- let create_proof_task_box l ~qed ~start =
+ let create_proof_task_box l ~qed ~start:lemma =
+ if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ vcs := create_property !vcs l (ProofTask { qed; lemma })
+ let create_error_bound_box ({ start; stop} as decl) name =
+ let l = nodes_in_slice ~start ~stop in
if not (topo_invariant l) then anomaly (str "overlapping boxes");
- vcs := create_property !vcs l (ProofTask { qed; start })
- let create_error_bound_box l ~switch =
- vcs := create_property !vcs l
- (ErrorBound { stuff = () })
+ vcs := create_property !vcs l (ErrorBound (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
- let delete_proof_task_box_of id =
- List.iter (fun x -> vcs := delete_property !vcs x)
- (List.filter (fun x ->
- match Dag.Property.data x with ProofTask _ -> true | _ -> false)
- (Vcs_.property_of !vcs id))
+ let delete_boxes_of id =
+ List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id)
let proof_task_box_of id =
match
CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id)
@@ -1046,6 +1066,66 @@ let _ = Errors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
+(****************** proof structure for error recovery ************************)
+(******************************************************************************)
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_expr;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+ static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+let proof_block_delimiters = ref []
+
+let register_proof_block_delimiter name static dynamic =
+ if List.mem_assoc name !proof_block_delimiters then
+ Errors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+ proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
+
+let mk_doc_node id = function
+ | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
+ Some { indentation; ast = expr; id }
+ | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } ->
+ Some { indentation; ast = expr; id }
+ | _ -> None
+let prev_node { id } =
+ let id = (VCS.visit id).next in
+ mk_doc_node id (VCS.visit id)
+let cur_node id = mk_doc_node id (VCS.visit id)
+
+let detect_proof_block id = function
+ | None -> ()
+ | Some name ->
+ match cur_node id with
+ | None -> ()
+ | Some entry_point -> try
+ let static, _ = List.assoc name !proof_block_delimiters in
+ begin match static { prev_node; entry_point } with
+ | None -> ()
+ | Some ({ start; stop } as decl) ->
+ VCS.create_error_bound_box decl name
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
+
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -1601,7 +1681,7 @@ end = struct (* {{{ *)
List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
Evd.(evar_context g))
then
- Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
+ Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
let (i, ast) = r_ast in
@@ -1609,12 +1689,12 @@ end = struct (* {{{ *)
vernac_interp r_state_fb ast;
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
- | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
+ | Evd.Evar_empty -> Errors.errorlabstrm "STM" (str "no progress")
| Evd.Evar_defined t ->
let t = Evarutil.nf_evar sigma t in
if Evarutil.is_ground_term sigma t then
t, Evd.evar_universe_context sigma
- else Errors.errorlabstrm "Stm" (str"The solution is not ground")
+ else Errors.errorlabstrm "STM" (str"The solution is not ground")
end) ()
in
RespBuiltSubProof (t,uc)
@@ -1897,6 +1977,53 @@ let log_processing_sync id name reason = log_string Printf.(sprintf
let wall_clock_last_fork = ref 0.0
let known_state ?(redefine_qed=false) ~cache id =
+
+ let error_absorbing_tactic id exn =
+ let boxes = VCS.box_of id in
+ let valid_boxes = CList.map_filter (function
+ | ErrorBound ({ stop } as decl, name) when Stateid.equal stop id ->
+ Some (decl, name)
+ | _ -> None) boxes in
+ assert(List.length valid_boxes < 2);
+ if valid_boxes = [] then iraise exn
+ else
+ let decl, name = List.hd valid_boxes in
+ try
+ let _, dynamic_check = List.assoc name !proof_block_delimiters in
+ match dynamic_check decl with
+ | `Leaks -> iraise exn
+ | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
+ let tac =
+ let open Proofview.Notations in
+ Proofview.Unsafe.tclSETGOALS goals_to_admit <*>
+ Proofview.give_up in
+ match (VCS.get_info base_state).state with
+ | Valid { proof } ->
+ Proof_global.unfreeze proof;
+ Proof_global.with_current_proof (fun _ p ->
+ Pp.feedback ~state_id:id Feedback.AddedAxiom;
+ fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ Option.iter (fun expr -> vernac_interp id {
+ verbose = true; loc = Loc.ghost; expr; indentation = 0;
+ strlen = 0 })
+ recovery_command
+ | _ -> assert false
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
+ in
+
+ (* Absorb tactic errors from f () *)
+ let resilient_tactic id f =
+ try f ()
+ with e when Errors.noncritical e ->
+ let ie = Errors.push e in
+ error_absorbing_tactic id ie in
+ (* Absorb errors from f x *)
+ let resilient_command f x =
+ try f x
+ with e when Errors.noncritical e -> () in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
@@ -1928,25 +2055,34 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
reach view.next), cache, true
| `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
- reach ~cache:`Shallow view.next;
- Hooks.(call tactic_being_run true);
- Partac.vernac_interp
- cancel !Flags.async_proofs_n_tacworkers view.next id x;
- Hooks.(call tactic_being_run false)
+ resilient_tactic id (fun () ->
+ reach ~cache:`Shallow view.next;
+ Hooks.(call tactic_being_run true);
+ Partac.vernac_interp
+ cancel !Flags.async_proofs_n_tacworkers view.next id x;
+ Hooks.(call tactic_being_run false))
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
reach view.next;
Query.vernac_interp cancel view.next id x
), cache, false
- | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
- reach view.next;
- if ctac then Hooks.(call tactic_being_run true);
+ | `Cmd { cast = x; ceff = eff; ctac = true } -> (fun () ->
+ resilient_tactic id (fun () ->
+ reach view.next;
+ Hooks.(call tactic_being_run true);
+ vernac_interp id x;
+ Hooks.(call tactic_being_run false));
+ if eff then update_global_env ()
+ ), (if eff then `Yes else cache), true
+ | `Cmd { cast = x; ceff = eff } -> (fun () ->
+ resilient_command reach view.next;
vernac_interp id x;
- if ctac then Hooks.(call tactic_being_run false);
- if eff then update_global_env ()), (if eff then `Yes else cache), true
+ if eff then update_global_env ()
+ ), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
- reach view.next; vernac_interp id x;
+ resilient_command reach view.next;
+ vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
@@ -2337,11 +2473,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
Backtrack.record ();
finish ();
`Ok
- | VtProofStep paral, w ->
+ | VtProofStep { parallel; proof_block_detection }, w ->
let id = VCS.new_node ~id:newtip () in
- let queue = if paral then `TacQueue (ref false) else `MainQueue in
+ let queue = if parallel then `TacQueue (ref false) else `MainQueue in
VCS.commit id (Cmd {
ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+ detect_proof_block id proof_block_detection;
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQed keep, w ->
let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2524,7 +2661,7 @@ let edit_at id =
| _ -> anomaly (str "ProofTask not ending with Qed") in
VCS.branch ~root:master_id ~pos:id
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
- VCS.delete_proof_task_box_of id;
+ VCS.delete_boxes_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
@@ -2545,7 +2682,7 @@ let edit_at id =
VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
(Option.default brname bn)
(no_edit brinfo.VCS.kind);
- VCS.delete_proof_task_box_of id;
+ VCS.delete_boxes_of id;
VCS.gc ();
VCS.print ();
if not !Flags.async_proofs_full then
@@ -2562,7 +2699,7 @@ let edit_at id =
| _ -> None in
match focused, VCS.proof_task_box_of id, branch_info with
| _, Some _, None -> assert false
- | false, Some { qed = qed_id ; start }, Some(mode,bn) ->
+ | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
let tip = VCS.cur_tip () in
if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
then reopen_branch start id mode qed_id tip bn
diff --git a/stm/stm.mli b/stm/stm.mli
index d825ff33e..20dd40bcd 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -20,7 +20,9 @@ open Loc
The sentence [s] is parsed in the state [ontop].
If [newtip] is provided, then the returned state id is guaranteed to be
[newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) ->
+val add :
+ ontop:Stateid.t -> ?newtip:Stateid.t ->
+ ?check:(vernac_expr located -> unit) ->
bool -> edit_id -> string ->
Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
@@ -96,6 +98,82 @@ module ProofTask : AsyncTaskQueue.Task
module TacTask : AsyncTaskQueue.Task
module QueryTask : AsyncTaskQueue.Task
+(** document structure customization *************************************** **)
+
+(* A proof block delimiter defines a syntactic delimiter for sub proofs
+ that, when contain an error, do not impact the rest of the proof.
+ While checking a proof, if an error occurs in a (valid) block then
+ processing can skip the entire block and go on to give feedback
+ on the rest of the proof.
+
+ static_block_detection and dynamic_block_validation are run when
+ the closing block marker is parsed/executed respectively.
+
+ static_block_detection is for example called when "}" is parsed and
+ declares a block containing all proof steps between it and the matching
+ "{".
+
+ dynamic_block_validation is called when an error "crosses" the "}" statement.
+ Depending on the nature of the goal focused by "{" the block may absorb the
+ error or not. For example if the focused goal occurs in the type of
+ another goal, then the block is leaky.
+ Note that one can design proof commands that need no dynamic validation.
+
+ Example of document:
+
+ .. { tac1. tac2. } ..
+
+ Corresponding DAG:
+
+ .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
+
+ Declaration of block [-------------------------------------------]
+
+ start = 5 the first state_id that could fail in the block
+ stop = 6 the node that may absorb the error
+ dynamic_switch = 4 dynamic check on this node
+ carry_on_data = () no need to carry extra data from static to dynamic
+ checks
+*)
+
+module DynBlockData : Dyn.S
+
+type static_block_declaration = {
+ start : Stateid.t;
+ stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
+}
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_expr;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+ static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+val register_proof_block_delimiter :
+ Vernacexpr.proof_block_name ->
+ static_block_detection ->
+ dynamic_block_error_recovery ->
+ unit
+
(** customization ********************************************************** **)
(* From the master (or worker, but beware that to install the hook
@@ -122,7 +200,8 @@ type state = {
proof : Proof_global.state;
shallow : bool
}
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+val state_of_id :
+ Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
(** read-eval-print loop compatible interface ****************************** **)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index b1df3c9ca..aa9907045 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,8 +21,9 @@ let string_of_vernac_type = function
| VtQed VtKeep -> "Qed(keep)"
| VtQed VtKeepAsAxiom -> "Qed(admitted)"
| VtQed VtDrop -> "Qed(drop)"
- | VtProofStep false -> "ProofStep"
- | VtProofStep true -> "ProofStep (parallel)"
+ | VtProofStep { parallel; proof_block_detection } ->
+ "ProofStep " ^ if parallel then "par " else "" ^
+ Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b,(id,route)) ->
"Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
@@ -93,7 +94,9 @@ let rec classify_vernac e =
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
| VtStm _ | VtProofMode _ ), _ as x -> x
- | VtQed _, _ -> VtProofStep false, VtNow
+ | VtQed _, _ ->
+ VtProofStep { parallel = false; proof_block_detection = None },
+ VtNow
| (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
@@ -110,7 +113,7 @@ let rec classify_vernac e =
| VernacSubproof _ | VernacEndSubproof
| VernacCheckGuard
| VernacUnfocused
- | VernacSolveExistential _ -> VtProofStep false, VtLater
+ | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
@@ -219,4 +222,4 @@ let rec classify_vernac e =
let classify_as_query =
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep false, VtLater
+let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 14:19:13 +0000