diff options
| -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 |