aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/newring.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8df061870..8d83ffc33 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -31,6 +31,8 @@ open Decl_kinds
open Entries
open Misctypes
+DECLARE PLUGIN "newring_plugin"
+
(****************************************************************************)
(* controlled reduction *)