From 0efde84daaa6b032e40a920a36793181724de87a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 Sep 2017 17:38:31 +0200
Subject: 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.
---
 theories/Init.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'theories/Init.v')

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.
-- 
cgit v1.2.3