aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 4492b854b4..b720b2e0a8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -83,8 +83,8 @@ let lookup_map map =
let protect_red map env sigma c =
let c = EConstr.Unsafe.to_constr c in
- kl (create_clos_infos all env)
- (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
+ EConstr.of_constr (kl (create_clos_infos all env)
+ (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c));;
let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None