diff options
| author | Pierre-Marie Pédrot | 2014-09-25 08:26:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-26 19:10:16 +0200 |
| commit | 38fbd7ca90ce3b852fa19b9706a00e64c5d73046 (patch) | |
| tree | e72ff92fc435458036b1edab2d81169d71359b96 /proofs/proofview.mli | |
| parent | 1dccd3509f62560c0a48189f5a3b67ab195deab0 (diff) | |
Adding a tclNEWGOALS primitive.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index c44707c1e7..cdc2db796c 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -262,6 +262,11 @@ val tclEFFECTS : Declareops.side_effects -> unit tactic (* Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic +(* [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, + appending them to the list of focussed goals. If a goal is already solved, + it is not added. Prefer the other primitives when possible. *) +val tclNEWGOALS : Goal.goal list -> unit tactic + (* Shelves all the goals under focus. The goals are placed on the shelf for later use (or being solved by side-effects). *) val shelve : unit tactic |