aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index e85c12c591..cd9137fd08 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -878,7 +878,7 @@ let _ = add_map "field_cond"
(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
-let _ = Redexpr.declare_red_expr "simpl_field_expr"
+let _ = Redexpr.declare_reduction "simpl_field_expr"
(protect_red "field")