Tentative fix for bug #3957.

Now that ML tactics are not dispatched according to the type of their arguments
anymore, one has to take care of the way potentially atomic tactics are handled.
This patch ensures that the atomic tactics generated by the TACTIC EXTEND
macro have the right length and the right order.

There may be very rare trouble if two ML tactics in the same entry are of the
form

"foo" x1 ... xn
"foo" y1 ... ym

where all xi and yi may be empty. I doubt that the legacy implementation
behaved well in this case anyway.

0 files changed, 0 insertions, 0 deletions