aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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 fa56313d8f..6ff6730235 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -95,7 +95,7 @@ let lookup_map map =
let protect_red map env sigma c =
kl (create_clos_infos betadeltaiota env)
- (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);;
+ (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;