diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:14:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:17:25 +0200 |
| commit | 1394bab8ba40dd4714e941586109fd88a79ef653 (patch) | |
| tree | fa07c5843d8d04c27e755374dbda357552a9f59f | |
| parent | 9ae9ac00b6882a9918eea3cb7d809424695d37ff (diff) | |
Put the "*_cast_no_check" tactics in the monad.
| -rw-r--r-- | ltac/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 16 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
3 files changed, 13 insertions, 11 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 3849a8440..4893e4097 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -43,11 +43,11 @@ TACTIC EXTEND exact_no_check END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ] + [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ] + [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] END TACTIC EXTEND casetype diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6bf5831f7..dc018a670 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1850,14 +1850,16 @@ let exact_check c = Sigma.Unsafe.of_pair (tac, sigma) end } -let vm_cast_no_check c gl = - let concl = Tacmach.pf_concl gl in - Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl - -let native_cast_no_check c gl = - let concl = Tacmach.pf_concl gl in - Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl +let cast_no_check cast c = + Proofview.Goal.enter { enter = begin fun gl -> + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + Refine.refine ~unsafe:true { run = begin fun sigma -> + Sigma.here (Term.mkCast (c, cast, concl)) sigma + end } + end } +let vm_cast_no_check c = cast_no_check Term.VMcast c +let native_cast_no_check c = cast_no_check Term.NATIVEcast c let exact_proof c = let open Tacmach.New in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2ffedf81a..12364d211 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -115,8 +115,8 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic val assumption : unit Proofview.tactic val exact_no_check : constr -> unit Proofview.tactic -val vm_cast_no_check : constr -> tactic -val native_cast_no_check : constr -> tactic +val vm_cast_no_check : constr -> unit Proofview.tactic +val native_cast_no_check : constr -> unit Proofview.tactic val exact_check : constr -> unit Proofview.tactic val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic |