Stream: Coq devs & plugin devs

Topic: When to group vernac command extend?

Li-yao (Apr 09 2022 at 19:00):

In a .mlg, what's the difference between having multiple VERNAC COMMAND EXTEND vs a single one? And what's the purpose of the name after EXTEND?

VERNAC COMMAND EXTEND ...
| [ "FOO" ] -> { ... }
| [ "BAR" ] -> { ... }
END

(* vs *)


VERNAC COMMAND EXTEND ...
| [ "FOO" ] -> { ... }
END

VERNAC COMMAND EXTEND ...
| [ "BAR" ] -> { ... }
END

Pierre-Marie Pédrot (Apr 09 2022 at 19:07):

This changes the factorization rules of the parsing engine

Pierre-Marie Pédrot (Apr 09 2022 at 19:07):

If your command are discriminated by their first entry it will be equivalent

Pierre-Marie Pédrot (Apr 09 2022 at 19:08):

(there is more factorization going on with the first variant)

Gaëtan Gilbert (Apr 09 2022 at 21:55):

what about the name?

Last updated: Oct 13 2024 at 01:02 UTC