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/vernacextend.ml | |
| 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/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2725516a76..e29086d726 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -54,7 +54,6 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) - | VtNoProof of (unit -> unit) | VtCloseProof of (lemma:Lemmas.t -> unit) | VtOpenProof of (unit -> Lemmas.t) |