diff options
| author | Emilio Jesus Gallego Arias | 2019-08-24 02:36:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-07 10:36:37 +0200 |
| commit | ebe43dddd50b96c8553e1fbdf3d26413eac47806 (patch) | |
| tree | 4f8a2a459fb90f68c434d75ae032bd797c7c6756 /stm | |
| parent | ef7cade43d514cb8f3d6022c298fdc467fcc4a33 (diff) | |
[vernac] Split vernacular translation and interpretation.
This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.
This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 1042061021..b60c9c3dad 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1056,7 +1056,7 @@ end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) + Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1083,7 +1083,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else begin stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - Vernacentries.interp ?verbosely:(Some verbose) ~st expr + Vernacinterp.interp ?verbosely:(Some verbose) ~st expr end (****************************** CRUFT *****************************************) @@ -1970,7 +1970,7 @@ end = struct (* {{{ *) let stm_fail ~st fail f = if fail then - Vernacentries.with_fail ~st f + Vernacinterp.with_fail ~st f else f () @@ -2891,7 +2891,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> Exninfo.iraise else - let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let proof_mode = Some (Vernacinterp.get_default_proof_mode ()) in let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8d600c2859..24976d8c1f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -51,7 +51,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; - Vernacentries.proof_mode_opt_name; + Vernacinterp.proof_mode_opt_name; Attributes.program_mode_option_name; Proof_using.proof_using_opt_name; ] |