diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 18:29:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | 178672504f1c92b162c2575b14034cc7b698b6a4 (patch) | |
| tree | cb2fe74b45291b6b62020c0cf3a7fdebac46d15f /vernac/vernacentries.mli | |
| parent | b42b7073e47f03b6e907ffe902c72c72d82dbada (diff) | |
[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.
We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 2e6477995a..71cc29b6e1 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -33,9 +33,8 @@ val interp : val make_cases : string -> string list list -(* XXX STATE: this type hints that restoring the state should be the - caller's responsibility *) -val with_fail : st:Vernacstate.t -> bool -> (unit -> Proof_global.t option) -> Proof_global.t option +(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) +val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit val command_focus : unit Proof.focus_kind |