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.ml45
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 856ec0db5..cd1d704dd 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -14,6 +14,11 @@ open Libnames
open Printer
open Newring_ast
open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "newring_plugin"