aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-06 17:01:57 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-06 17:01:57 -0400
commiteb6f1f415868acca3a0cdb3837b2871b0907fe5f (patch)
tree0797c3f0374ca90b37fa8dbeeb44ecf2c7b8f9fd /src/Util/Tactics
parentcdee97867540fdfdfc6fa9f2c581eb99204adfcd (diff)
Faster clear_all tactic
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r--src/Util/Tactics/ClearAll.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Tactics/ClearAll.v b/src/Util/Tactics/ClearAll.v
index 96c208876..50b1e4179 100644
--- a/src/Util/Tactics/ClearAll.v
+++ b/src/Util/Tactics/ClearAll.v
@@ -1,4 +1,5 @@
Ltac clear_all :=
+ clear;
repeat match goal with
| [ H : _ |- _ ] => clear H
end.