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 /configure.ml | |
| 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 'configure.ml')
0 files changed, 0 insertions, 0 deletions