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/micromega/g_micromega.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/micromega')

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