diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 98b77ab35..3849a8440 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -39,7 +39,7 @@ TACTIC EXTEND cut END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ] + [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] END TACTIC EXTEND vm_cast_no_check diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5e0153fce..7acdff9ac 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let (sigma, c_interp) = pf_interp_casted_constr ist gl c in - Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma) + Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma) end } end | TacApply (a,ev,cb,cl) -> |