diff options
| -rw-r--r-- | proofs/refiner.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a66ab60819..cafc4100f2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -125,7 +125,8 @@ let start_tac gls = let finish_tac (sigr,gl) = repackage sigr gl -(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) let thens3parts_tac tacfi tac tacli (sigr,gs) = let nf = Array.length tacfi in let nl = Array.length tacli in |