From 975e7cd2ad032668c7df690c9bdaa8cdbb196569 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Sep 2016 16:09:17 +0200
Subject: Moving Ltac-specific generic arguments to their own file in the ltac/
 folder.

---
 plugins/firstorder/g_ground.ml4     | 1 +
 plugins/micromega/g_micromega.ml4   | 1 +
 plugins/quote/g_quote.ml4           | 1 +
 plugins/setoid_ring/g_newring.ml4   | 1 +
 plugins/ssrmatching/ssrmatching.ml4 | 1 +
 5 files changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09cb..4871626875 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -16,6 +16,7 @@ open Tacticals
 open Tacinterp
 open Libnames
 open Constrarg
+open Tacarg
 open Stdarg
 open Pcoq.Prim
 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 027f690fca..aadcf060e1 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -17,6 +17,7 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Constrarg
+open Tacarg
 
 DECLARE PLUGIN "micromega_plugin"
 
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fd87d5b7d3..ebd19428f0 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,6 +14,7 @@ open Tacexpr
 open Geninterp
 open Quote
 open Constrarg
+open Tacarg
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1a00200318..13e2254044 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -16,6 +16,7 @@ open Newring_ast
 open Newring
 open Stdarg
 open Constrarg
+open Tacarg
 open Pcoq.Constr
 open Pltac
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 150be9d727..099918c35e 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -20,6 +20,7 @@ open Pp
 open Pcoq
 open Genarg
 open Constrarg
+open Tacarg
 open Term
 open Vars
 open Topconstr
-- 
cgit v1.2.3