From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/nsatz/g_nsatz.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8da..195dec362 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -1,5 +1,3 @@
-DECLARE PLUGIN "nsatz_plugin"
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
@@ -10,6 +8,8 @@ DECLARE PLUGIN "nsatz_plugin"
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-- 
cgit v1.2.3