diff options
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 617ee4bed4..2888f16f1a 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -104,8 +104,7 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) - (Some((all_occurrences_expr,id),InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));; TACTIC EXTEND protect_fv |