From 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 22 May 2018 04:57:00 +0200
Subject: [api] Misctypes removal: move Tactypes to proofs

This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
---
 plugins/funind/g_indfun.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 24d1a40c2..9899b7b21 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,6 +15,7 @@ open Indfun_common
 open Indfun
 open Genarg
 open Stdarg
+open Tacarg
 open Tactypes
 open Pcoq
 open Pcoq.Prim
-- 
cgit v1.2.3