From dba567555fed9c88887b463a975c3d7e0852ebd3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Oct 2018 19:17:47 +0200
Subject: Plug ARGUMENT EXTEND into the argument extension API.

---
 plugins/firstorder/g_ground.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index ff106404c8..db753fc672 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -123,7 +123,6 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
-open Genarg
 open Ppconstr
 open Printer
 let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
-- 
cgit v1.2.3