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 | |
| parent | 1dccd3509f62560c0a48189f5a3b67ab195deab0 (diff) | |
Adding a tclNEWGOALS primitive.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 7 | ||||
| -rw-r--r-- | proofs/proofview.mli | 5 |
2 files changed, 12 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6ecf4da7e6..e63db14ab8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -538,6 +538,13 @@ let tclINDEPENDENT tac = | [_] -> tac | _ -> list_iter_goal () (fun _ () -> tac) +let tclNEWGOALS gls = + Proof.modify begin fun step -> + let map gl = Goal.advance step.solution gl in + let gls = List.map_filter map gls in + { step with comb = step.comb @ gls } + end + (* No backtracking can happen here, hence, as opposed to the dispatch tacticals, everything is done in one step. *) let sensitive_on_proofview s env step = 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 |