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 /theories/Init.v | |
| 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 'theories/Init.v')
| -rw-r--r-- | theories/Init.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Init.v b/theories/Init.v index 04394e2c5d..16e7d7a6f9 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -8,8 +8,6 @@ Declare ML Module "ltac2_plugin". -Global Set Default Proof Mode "Ltac2". - (** Primitive types *) Ltac2 Type int. |