From 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 8 Mar 2017 03:22:22 +0100
Subject: [camlpX] Remove camlp4 compat layer.

We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.

We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
---
 plugins/funind/g_indfun.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 368b23be30..cf2e42d2c9 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
-open Compat
 open Util
 open Term
 open Pp
@@ -17,6 +16,7 @@ open Indfun
 open Genarg
 open Stdarg
 open Misctypes
+open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
-- 
cgit v1.2.3