From 975e7cd2ad032668c7df690c9bdaa8cdbb196569 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/firstorder/g_ground.ml4')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09c..487162687 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
 
-- 
cgit v1.2.3