aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh9
-rw-r--r--dev/top_printers.ml4
-rw-r--r--plugins/derive/g_derive.mlg2
-rw-r--r--plugins/funind/g_indfun.mlg10
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_ltac.mlg7
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg8
-rw-r--r--stm/stm.ml26
-rw-r--r--stm/vernac_classifier.ml108
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--vernac/vernacextend.ml19
-rw-r--r--vernac/vernacextend.mli13
13 files changed, 106 insertions, 108 deletions
diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
new file mode 100644
index 0000000000..c5f1510357
--- /dev/null
+++ b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then
+
+ mtac2_CI_REF=vernac-when-sideff
+ mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+ equations_CI_REF=vernac-when-sideff
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4ce87faaa1..87b4d31054 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -533,7 +533,7 @@ let _ =
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
- let cmd_class _ = VtQuery,VtNow in
+ let cmd_class _ = VtQuery in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintConstr" [cmd]
@@ -542,7 +542,7 @@ let _ =
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
- let cmd_class _ = VtQuery,VtNow in
+ let cmd_class _ = VtQuery in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintPureConstr" [cmd]
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 6c9cd66f96..de3fb9f11f 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin"
{
-let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 833ff9f1ed..c217ed8b1d 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,14 +186,14 @@ let classify_as_Fixpoint recsl =
let classify_funind recsl =
match classify_as_Fixpoint recsl with
- | Vernacextend.VtSideff ids, _
+ | Vernacextend.VtSideff (ids, _)
when is_proof_termination_interactively_checked recsl ->
- Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
+ Vernacextend.(VtStartProof (GuaranteesOpacity, ids))
| x -> x
let is_interactive recsl =
match classify_funind recsl with
- | Vernacextend.VtStartProof _, _ -> true
+ | Vernacextend.VtStartProof _ -> true
| _ -> false
}
@@ -243,7 +243,7 @@ let warning_error names e =
VERNAC COMMAND EXTEND NewFunctionalScheme
| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
- => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
+ => { Vernacextend.(VtSideff(List.map pi1 fas, VtLater)) }
->
{ begin
try
@@ -275,7 +275,7 @@ END
VERNAC COMMAND EXTEND NewFunctionalCase
| ["Functional" "Case" fun_scheme_arg(fas) ]
- => { Vernacextend.(VtSideff[pi1 fas], VtLater) }
+ => { Vernacextend.(VtSideff([pi1 fas], VtLater)) }
-> { Functional_principles_types.build_case_scheme fas }
END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7691ca225e..7ba63f1830 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -336,7 +336,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
let add_hints base = add_rew_rules base eqs in
List.iter add_hints bases
-let classify_hint _ = VtSideff [], VtLater
+let classify_hint _ = VtSideff ([], VtLater)
}
@@ -422,7 +422,7 @@ END
open Inv
open Leminv
-let seff id = VtSideff [id], VtLater
+let seff id = VtSideff ([id], VtLater)
}
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d10d10a664..afdea98ef5 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -446,8 +446,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
let solving_tac = is_explicit_terminator t in
let parallel = `Yes (solving_tac,anon_abstracting_tac) in
let pbr = if solving_tac then Some "par" else None in
- VtProofStep{ parallel = parallel; proof_block_detection = pbr },
- VtLater
+ VtProofStep{ parallel = parallel; proof_block_detection = pbr }
} -> {
let t = rm_abstract t in
vernac_solve Goal_select.SelectAll n t def
@@ -494,7 +493,7 @@ END
VERNAC COMMAND EXTEND VernacTacticNotation
| #[ deprecation; locality; ]
[ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
- { VtSideff [], VtNow } ->
+ { VtSideff ([], VtNow) } ->
{
let n = Option.default 0 n in
Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
@@ -542,7 +541,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
VtSideff (List.map (function
| TacticDefinition ({CAst.v=r},_) -> r
- | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
+ | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater)
} -> {
Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
}
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 58c8dabd79..62bc2a9259 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,7 @@ open Obligations
let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
-let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 1a84158df7..1cc333945d 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -277,19 +277,19 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
add_setoid atts binders a aeq t n
}
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
- => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity, [n]) }
-> { if Lib.is_modtype () then
CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
add_morphism_interactive atts m n }
| #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ]
- => { VtSideff([n]), VtLater }
+ => { VtSideff([n], VtLater) }
-> { add_morphism_as_parameter atts m n }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]) }
-> { add_morphism atts [] m s n }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]) }
-> { add_morphism atts binders m s n }
END
diff --git a/stm/stm.ml b/stm/stm.ml
index 1e89d6937c..d77e37c910 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1563,7 +1563,7 @@ end = struct (* {{{ *)
let perform_states query =
if query = [] then [] else
let is_tac e = match Vernac_classifier.classify_vernac e with
- | VtProofStep _, _ -> true
+ | VtProofStep _ -> true
| _ -> false
in
let initial =
@@ -2860,12 +2860,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
" classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
match c with
(* Meta *)
- | VtMeta, _ ->
+ | VtMeta ->
let id = Backtrack.undo_vernac_classifier expr ~doc in
process_back_meta_command ~newtip ~head id x
(* Query *)
- | VtQuery, w ->
+ | VtQuery ->
let id = VCS.new_node ~id:newtip proof_mode () in
let queue =
if VCS.is_vio_doc () &&
@@ -2875,10 +2875,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
VCS.set_parsing_state id head_parsing;
- Backtrack.record (); assert (w == VtLater); `Ok
+ Backtrack.record (); `Ok
(* Proof *)
- | VtStartProof (guarantee, names), w ->
+ | VtStartProof (guarantee, names) ->
if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
"Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
@@ -2900,9 +2900,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
VCS.set_parsing_state id head_parsing;
- Backtrack.record (); assert (w == VtLater); `Ok
+ Backtrack.record (); `Ok
- | VtProofStep { parallel; proof_block_detection = cblock }, w ->
+ | VtProofStep { parallel; proof_block_detection = cblock } ->
let id = VCS.new_node ~id:newtip proof_mode () in
let queue =
match parallel with
@@ -2914,18 +2914,18 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
detection should occur here.
detect_proof_block id cblock; *)
VCS.set_parsing_state id head_parsing;
- Backtrack.record (); assert (w == VtLater); `Ok
+ Backtrack.record (); `Ok
- | VtQed keep, w ->
+ | VtQed keep ->
let valid = VCS.get_branch_pos head in
let rc =
merge_proof_branch ~valid ~id:newtip x keep head in
VCS.checkout_shallowest_proof_branch ();
- Backtrack.record (); assert (w == VtLater);
+ Backtrack.record ();
rc
(* Side effect in a (still open) proof is replayed on all branches*)
- | VtSideff l, w ->
+ | VtSideff (l, w) ->
let id = VCS.new_node ~id:newtip proof_mode () in
let new_ids =
match (VCS.get_branch head).VCS.kind with
@@ -2961,15 +2961,13 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
VCS.set_parsing_state id parsing_state) new_ids;
`Ok
- | VtProofMode pm, VtNow ->
+ | VtProofMode pm ->
let proof_mode = Pvernac.lookup_proof_mode pm in
let id = VCS.new_node ~id:newtip proof_mode () in
VCS.commit id (mkTransCmd x [] false `MainQueue);
VCS.set_parsing_state id head_parsing;
Backtrack.record (); `Ok
- | VtProofMode _, VtLater ->
- anomaly(str"classifier: VtProofMode must imply VtNow.")
end in
let pr_rc rc = match rc with
| `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa16f9535d..cfeca1fa62 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -20,9 +20,13 @@ let string_of_parallel = function
"par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
| `No -> ""
-let string_of_vernac_type = function
+let string_of_vernac_when = function
+ | VtLater -> "Later"
+ | VtNow -> "Now"
+
+let string_of_vernac_classification = function
| VtStartProof _ -> "StartProof"
- | VtSideff _ -> "Sideff"
+ | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
| VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
| VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
| VtQed VtDrop -> "Qed(drop)"
@@ -33,13 +37,6 @@ let string_of_vernac_type = function
| VtMeta -> "Meta "
| VtProofMode _ -> "Proof Mode"
-let string_of_vernac_when = function
- | VtLater -> "Later"
- | VtNow -> "Now"
-
-let string_of_vernac_classification (t,w) =
- string_of_vernac_type t ^ " " ^ string_of_vernac_when w
-
let vtkeep_of_opaque = let open Proof_global in function
| Opaque -> VtKeepOpaque
| Transparent -> VtKeepDefined
@@ -67,15 +64,15 @@ let classify_vernac e =
| VernacSetOption (_, l,_)
when CList.exists (CList.equal String.equal l)
options_affecting_stm_scheduling ->
- VtSideff [], VtNow
+ VtSideff ([], VtNow)
(* Qed *)
- | VernacAbort _ -> VtQed VtDrop, VtLater
- | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater
- | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater
- | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater
+ | VernacAbort _ -> VtQed VtDrop
+ | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
+ | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
+ | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
- | VernacCheckMayEval _ -> VtQuery, VtLater
+ | VernacCheckMayEval _ -> VtQuery
(* ProofStep *)
| VernacProof _
| VernacFocus _ | VernacUnfocus
@@ -83,27 +80,25 @@ let classify_vernac e =
| VernacCheckGuard
| VernacUnfocused
| VernacSolveExistential _ ->
- VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
+ VtProofStep { parallel = `No; proof_block_detection = None }
| VernacBullet _ ->
- VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
- VtLater
+ VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }
| VernacEndSubproof ->
VtProofStep { parallel = `No;
- proof_block_detection = Some "curly" },
- VtLater
+ proof_block_detection = Some "curly" }
(* StartProof *)
| VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
- VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+ VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
| VernacDefinition (_,({v=i},_),ProveBody _) ->
let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof(guarantee, idents_of_name i), VtLater
+ VtStartProof(guarantee, idents_of_name i)
| VernacStartTheoremProof (_,l) ->
let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let ids = List.map (fun (({v=i}, _), _) -> i) l in
let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof (guarantee,ids), VtLater
+ VtStartProof (guarantee,ids)
| VernacFixpoint (discharge,l) ->
let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee =
@@ -114,8 +109,8 @@ let classify_vernac e =
List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof (guarantee,ids), VtLater
- else VtSideff ids, VtLater
+ then VtStartProof (guarantee,ids)
+ else VtSideff (ids, VtLater)
| VernacCoFixpoint (discharge,l) ->
let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee =
@@ -126,15 +121,15 @@ let classify_vernac e =
List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof (guarantee,ids), VtLater
- else VtSideff ids, VtLater
+ then VtStartProof (guarantee,ids)
+ else VtSideff (ids, VtLater)
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
- VtSideff ids, VtLater
+ VtSideff (ids, VtLater)
| VernacPrimitive (id,_,_) ->
- VtSideff [id.CAst.v], VtLater
- | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+ VtSideff ([id.CAst.v], VtLater)
+ | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
| VernacInductive (_, _,_,l) ->
let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
@@ -142,12 +137,12 @@ let classify_vernac e =
CList.map_filter (function
| AssumExpr({v=Names.Name n},_), _ -> Some n
| _ -> None) l) l in
- VtSideff (List.flatten ids), VtLater
+ VtSideff (List.flatten ids, VtLater)
| VernacScheme l ->
let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
- VtSideff ids, VtLater
- | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
- | VernacBeginSection {v=id} -> VtSideff [id], VtLater
+ VtSideff (ids, VtLater)
+ | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
+ | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
| VernacUniverse _ | VernacConstraint _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
@@ -166,17 +161,17 @@ let classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _
- | VernacDeclareInstance _ -> VtSideff [], VtLater
+ | VernacDeclareInstance _ -> VtSideff ([], VtLater)
(* Who knows *)
- | VernacLoad _ -> VtSideff [], VtNow
+ | VernacLoad _ -> VtSideff ([], VtNow)
(* (Local) Notations have to disappear *)
- | VernacEndSegment _ -> VtSideff [], VtNow
+ | VernacEndSegment _ -> VtSideff ([], VtNow)
(* Modules with parameters have to be executed: can import notations *)
| VernacDeclareModule (exp,{v=id},bl,_)
| VernacDefineModule (exp,{v=id},bl,_,_) ->
- VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+ VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
| VernacDeclareModuleType ({v=id},bl,_,_) ->
- VtSideff [id], if bl = [] then VtLater else VtNow
+ VtSideff ([id], if bl = [] then VtLater else VtNow)
(* These commands alter the parser *)
| VernacDeclareCustomEntry _
| VernacOpenCloseScope _ | VernacDeclareScope _
@@ -186,40 +181,39 @@ let classify_vernac e =
| VernacSyntacticDefinition _
| VernacRequire _ | VernacImport _ | VernacInclude _
| VernacDeclareMLModule _
- | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
- | VernacProofMode pm -> VtProofMode pm, VtNow
+ | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+ | VernacProofMode pm -> VtProofMode pm
| VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
+ VtStartProof (guarantee, idents_of_name name.CAst.v)
| VernacInstance ((name,_),_,_,_,_) ->
- VtSideff (idents_of_name name.CAst.v), VtLater
+ VtSideff (idents_of_name name.CAst.v, VtLater)
(* Stm will install a new classifier to handle these *)
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
| VernacResetName _ | VernacResetInitial
- | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+ | VernacBackTo _ | VernacRestart -> VtMeta
(* What are these? *)
| VernacRestoreState _
- | VernacWriteState _ -> VtSideff [], VtNow
+ | VernacWriteState _ -> VtSideff ([], VtNow)
(* Plugins should classify their commands *)
| VernacExtend (s,l) ->
try Vernacextend.get_vernac_classifier s l
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let rec static_control_classifier v = v |> CAst.with_val (function
- | VernacExpr (atts, e) ->
- static_classifier ~atts e
- | VernacTimeout (_,e) -> static_control_classifier e
- | VernacTime (_,e) | VernacRedirect (_, e) ->
- static_control_classifier e
- | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ | VernacExpr (atts, e) ->
+ static_classifier ~atts e
+ | VernacTimeout (_,e) -> static_control_classifier e
+ | VernacTime (_,e) | VernacRedirect (_, e) ->
+ static_control_classifier e
+ | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (* XXX why is Fail not always Query? *)
(match static_control_classifier e with
- | ( VtQuery | VtProofStep _ | VtSideff _
- | VtMeta), _ as x -> x
- | VtQed _, _ ->
- VtProofStep { parallel = `No; proof_block_detection = None },
- VtLater
- | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
+ | VtQuery | VtProofStep _ | VtSideff _
+ | VtMeta as x -> x
+ | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
+ | VtStartProof _ | VtProofMode _ -> VtQuery))
in
static_control_classifier e
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index bd1f925486..930be257e3 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -884,7 +884,7 @@ END
{
let classify_ltac2 = function
-| StrSyn _ -> Vernacextend.(VtSideff [], VtNow)
+| StrSyn _ -> Vernacextend.(VtSideff ([], VtNow))
| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ -> Vernacextend.classify_as_sideeff
}
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 6a52177dd5..c7008c2a84 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -37,7 +41,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -48,11 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
type typed_vernac =
| VtDefault of (unit -> unit)
@@ -130,9 +129,9 @@ let get_vernac_classifier (name, i) args =
let declare_vernac_classifier name f =
classifiers := String.Map.add name f !classifiers
-let classify_as_query = VtQuery, VtLater
-let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
+let classify_as_query = VtQuery
+let classify_as_sideeff = VtSideff ([], VtLater)
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}
type (_, _) ty_sig =
| TyNil : (vernac_command, vernac_classification) ty_sig
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 78b7f21b0d..fd59d77237 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -53,7 +57,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -64,11 +68,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
(** Interpretation of extended vernac phrases. *)
type typed_vernac =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:35:00 +0000