aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/g_newring.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring/g_newring.ml4')
-rw-r--r--plugins/setoid_ring/g_newring.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1ebb6e6b7..f5a734048 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -16,7 +16,6 @@ open Newring_ast
open Newring
open Stdarg
open Constrarg
-open Pcoq.Prim
open Pcoq.Constr
open Pcoq.Tactic