diff options
| author | Pierre-Marie Pédrot | 2016-05-16 20:57:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:17:25 +0200 |
| commit | 9ae9ac00b6882a9918eea3cb7d809424695d37ff (patch) | |
| tree | ee44e2e88516143ce366e7b4ec4be3acc96bc8b1 /ltac | |
| parent | 12f4c8ed277fa8368cab2e99f173339a64bcef3d (diff) | |
Put the "exact" family of tactic in the monad.
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 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"<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) -> |