diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 7 |
1 files changed, 7 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 = |