From 9ae9ac00b6882a9918eea3cb7d809424695d37ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 20:57:34 +0200 Subject: Put the "exact" family of tactic in the monad. --- ltac/coretactics.ml4 | 2 +- ltac/tacinterp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 98b77ab357..3849a84405 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 5e0153fcee..7acdff9acf 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"") 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) -> -- cgit v1.2.3