diff options
| author | Pierre-Marie Pédrot | 2017-09-02 17:38:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-02 17:44:01 +0200 |
| commit | 0efde84daaa6b032e40a920a36793181724de87a (patch) | |
| tree | 3e0fba38563bb730c7980e828370cda2b698ef39 /src/tac2stdlib.ml | |
| parent | 1f7a2ea0e0513620bb946c10923d38f845061afa (diff) | |
Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.
Instead of setting globally the option, we add a hook to set it in
the init object of the plugin.
Diffstat (limited to 'src/tac2stdlib.ml')
0 files changed, 0 insertions, 0 deletions