diff options
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 |