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 /vernac/vernacentries.mli | |
| 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 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 29 |
1 files changed, 5 insertions, 24 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e65f9d3cfe..6368ebeed8 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,25 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The main interpretation function of vernacular expressions *) -val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t - -(** Execute a Qed but with a proof_object which may contain a delayed - proof and won't be forced *) -val interp_qed_delayed_proof - : proof:Proof_global.proof_object - -> info:Lemmas.Info.t - -> st:Vernacstate.t - -> control:Vernacexpr.control_flag list - -> Vernacexpr.proof_end CAst.t - -> Vernacstate.t - -(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) -val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit - -(** Flag set when the test-suite is called. Its only effect to display - verbose information for [Fail] *) -val test_mode : bool ref +(** Vernac Translation into the Vernac DSL *) +val translate_vernac + : atts:Attributes.vernac_flags + -> Vernacexpr.vernac_expr + -> Vernacextend.typed_vernac (** Vernacular require command *) val vernac_require : @@ -38,8 +24,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind - -(** Default proof mode set by `start_proof` *) -val get_default_proof_mode : unit -> Pvernac.proof_mode - -val proof_mode_opt_name : string list |