aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index dd68eac24c..6e072e8317 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -279,8 +279,6 @@ let my_constant c =
let my_reference c =
lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
-let new_ring_path =
- DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
let znew_ring_path =
DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =