diff options
| author | Arnaud Spiwack | 2014-10-17 15:31:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:44 +0200 |
| commit | cadfe23210c8edaab1f22d0edb7acc33fb9ff782 (patch) | |
| tree | 50a7a8942285cdbf9555122c0abfa03e493afec6 /tactics/rewrite.ml | |
| 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 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b55ee7030b..ec9a9ff3e7 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1478,13 +1478,13 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = match is_hyp, prf with | Some id, Some p -> let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.tclNEWGOALS gls in - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> convert_hyp_no_check (id, None, newt) | None, Some p -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let make sigma = @@ -1494,7 +1494,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = Proofview.Refine.refine make <*> Proofview.tclNEWGOALS gls end | None, None -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in |