diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-17 16:24:37 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-17 16:27:35 +0200 |
| commit | 42cbdfccf0c0500935d619dccaa00476690229f8 (patch) | |
| tree | c72ac918e55c7a9ef6d3b74ba0e2c6f0cc3efe29 /intf/vernacexpr.mli | |
| parent | 905e82c498d920ff5508d57c5af4a3a8e939f2a8 (diff) | |
par: like all: but in parallel
This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.
`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.
`par: abstract tac` runs abstract on the generated proof terms. Nested
abstract calls are not supported.
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 45d71e32b..1c75d76dd 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -484,9 +484,11 @@ and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : bool; + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } +and solving_tac = bool (* a terminator *) +and anon_abstracting_tac = bool (* abstracting anonymously its result *) and proof_block_name = string (* open type of delimiters *) type vernac_when = | VtNow |