From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 17:34:12 +0200
Subject: Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
---
 plugins/decl_mode/decl_interp.ml      | 1 +
 plugins/decl_mode/decl_proof_instr.ml | 1 +
 plugins/decl_mode/g_decl_mode.ml4     | 1 +
 plugins/decl_mode/ppdecl_proof.ml     | 1 +
 4 files changed, 4 insertions(+)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f68c01b18b..2b63ed6d6e 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Names
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e19dc86c45..deb2ede1d5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Pp
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 18a35c6cfb..a71d20f0dc 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "decl_mode_plugin"
 
+open Ltac_plugin
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2d..f5de638ed2 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Pp
 open Decl_expr
-- 
cgit v1.2.3