aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/derive')
-rw-r--r--plugins/derive/g_derive.ml42
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 35a5a7616..39cad4d03 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -7,8 +7,6 @@
(************************************************************************)
open Constrarg
-open Pcoq.Prim
-open Pcoq.Constr
(*i camlp4deps: "grammar/grammar.cma" i*)