aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrparser.ml41
-rw-r--r--plugins/ssr/ssrvernac.ml41
2 files changed, 0 insertions, 2 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index e4a0910673..319f58931a 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -15,7 +15,6 @@ open Names
open Pp
open Pcoq
open Ltac_plugin
-open Genarg
open Stdarg
open Tacarg
open Libnames
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index d62656f95f..02a5d08507 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -25,7 +25,6 @@ open Notation_ops
open Notation_term
open Glob_term
open Stdarg
-open Genarg
open Decl_kinds
open Pp
open Ppconstr