Do these do anything?
#[global] Declare ML Module "ltac_plugin".
#[local] Declare ML Module "ltac_plugin".
Local Declare ML Module "ltac_plugin".
Global Declare ML Module "ltac_plugin".
I'm under the impression that they are all equivalent.
Global is default
Local is module local
Local is also possibly buggy as I don't think anyone uses it
Last updated: Mar 29 2024 at 15:02 UTC