diff options
| author | Pierre-Marie Pédrot | 2016-05-17 10:47:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 10:50:02 +0200 |
| commit | cddddce068bc0482f62ffab8e412732a307b90bb (patch) | |
| tree | 5aa27798bb952b6ec8e9af0d59ba31ebfd55ceb8 /ltac | |
| parent | ed1c4d01388bf11710b38f1c302d405233c24647 (diff) | |
Put the "move" tactic in the monad.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index b7fc63cd56..ce28eacc09 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -200,10 +200,10 @@ END (** Move *) TACTIC EXTEND move - [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ] -| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ] -| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ] -| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ] + [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ] +| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ] +| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ] +| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] END (** Revert *) |