diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 14:26:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 14:43:10 +0100 |
| commit | 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (patch) | |
| tree | c139ad543105cfea7791aab2831f5623cddb4a5e /tactics/rewrite.ml | |
| parent | 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 (diff) | |
Moving conversion functions to the new tactic API.
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d0a090e5c..8b71affff 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1569,10 +1569,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = convert_concl_no_check newt DEFAULTcast in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in + let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in let opt_beta = match clause with | None -> Proofview.tclUNIT () - | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) + | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp) in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in |