From 548dcdc751287274c9cce7d13d779a81346a5af2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 22 Nov 2018 11:44:12 +0100
Subject: Remove the unsafe camlp5 API from the Coq codebase.

---
 plugins/funind/g_indfun.mlg | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 7e707b423a..8f0440a2a4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -145,7 +145,6 @@ END
 
 {
 
-module Gram = Pcoq.Gram
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
-- 
cgit v1.2.3