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 3f69701bd3..b02b97f656 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -89,10 +89,10 @@ let protect_red map env sigma c0 =
EConstr.of_constr (eval 0 c)
let protect_tac map =
- Tactics.reduct_option (protect_red map,DEFAULTcast) None
+ Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
+ Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
(****************************************************************************)