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/ltac/extraargs.ml4 | 1 -
 plugins/ltac/g_auto.ml4    | 1 -
 plugins/ltac/g_class.ml4   | 2 --
 3 files changed, 4 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 0c6d10bf8c..4de27e8138 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Pp
-open Genarg
 open Stdarg
 open Tacarg
 open Pcoq.Prim
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 8eadb66edc..6913543c9a 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -10,7 +10,6 @@
 
 open Pp
 open Constr
-open Genarg
 open Stdarg
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 1c2f90b670..265368833b 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -32,8 +32,6 @@ VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
     set_transparency cl false ]
 END
 
-open Genarg
-
 let pr_debug _prc _prlc _prt b =
   if b then Pp.str "debug" else Pp.mt()
 
-- 
cgit v1.2.3