diff options
| author | Pierre-Marie Pédrot | 2016-05-13 00:16:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:17:24 +0200 |
| commit | 73cdb000ec07ec484557839c4b94fcf779df2f06 (patch) | |
| tree | 4aa04d713d26b537c187e1be801b4788d4a4e915 /ltac | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
Put the "clear" tactic into the monad.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tauto.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 8b5f527cd0..4e2dfafb52 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -247,7 +247,7 @@ END TACTIC EXTEND clear [ "clear" hyp_list(ids) ] -> [ if List.is_empty ids then Tactics.keep [] - else Proofview.V82.tactic (Tactics.clear ids) + else Tactics.clear ids ] | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] END diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 655bfd5f52..c0cae84c02 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -102,7 +102,7 @@ let assert_ ?by c = let apply c = Tactics.apply c -let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl) +let clear id = Tactics.clear [id] let assumption = Tactics.assumption |