aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/coretactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/coretactics.ml4')
-rw-r--r--tactics/coretactics.ml46
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index ab97dad70..b68aab621 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -216,6 +216,12 @@ TACTIC EXTEND clear
| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
END
+(* Clearbody *)
+
+TACTIC EXTEND clearbody
+ [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+END
+
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
open Tacexpr