Remove the syntax [Vernac1. Vernac2. … Vernacn. ].

It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.

The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].

I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.

0 files changed, 0 insertions, 0 deletions