diff options
| author | Emilio Jesus Gallego Arias | 2019-06-07 15:22:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-26 12:27:04 +0200 |
| commit | d4aeb1ef92a9fc35b242a0d91488de60c24d7bbb (patch) | |
| tree | 0c4165866165937fae20b0dfe9a334e55ea3b8b8 /vernac/vernacentries.mli | |
| parent | 2c39a12f5a8d7178b991595324692c1596ea9199 (diff) | |
[stm] [vernac] Remove special ?proof parameter from vernac main path
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index ad3e9f93d9..3563e9984a 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -20,10 +20,17 @@ val vernac_require : Libnames.qualid option -> bool option -> Libnames.qualid list -> unit (** The main interpretation function of vernacular expressions *) -val interp : - ?verbosely:bool -> - ?proof:(Proof_global.proof_object * Lemmas.Info.t) -> - st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t +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 + -> ?loc:Loc.t + -> Vernacexpr.proof_end + -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |