diff options
author | 2014-10-17 15:31:58 +0200 | |
---|---|---|
committer | 2014-10-22 07:31:44 +0200 | |
commit | cadfe23210c8edaab1f22d0edb7acc33fb9ff782 (patch) | |
tree | 50a7a8942285cdbf9555122c0abfa03e493afec6 /plugins/setoid_ring/newring.ml4 | |
parent | d76c6d9c92d8486ef4b672f9b44e5c6ea782d7ff (diff) |
Proofview: split [V82] module into [Unsafe] and [V82].
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b28f0652d..2006a2a61 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -834,7 +834,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = let rl = carg (make_term_list env evdref e.ring_carrier rl) in let lH = carg (make_hyp_list env evdref lH) in let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end @@ -1150,7 +1150,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t = let rl = carg (make_term_list env evdref e.field_carrier rl) in let lH = carg (make_hyp_list env evdref lH) in let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end |