diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-02 11:40:49 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-02 11:40:49 -0700 |
| commit | 2f667be402bb86e8f79c599ef12072659d19ebe2 (patch) | |
| tree | e2758b1fd11fe47c4485f826631a563d71793052 /src/Util/Tactics.v | |
| parent | 30061ea70b84286a7d2a5d23cd01445ac1b695ee (diff) | |
Add [idtac_goal]
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 23a4bd95e..6c48dbd98 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -451,3 +451,10 @@ Ltac cfail msg := constr:(_ : cfail msg). Ltac cidtac msg := constr:(_ : cidtac msg). Ltac cidtac2 msg1 msg2 := constr:(_ : cidtac2 msg1 msg2). Ltac cidtac3 msg1 msg2 msg3 := constr:(_ : cidtac2 msg1 msg2 msg3). + +Ltac idtac_goal := lazymatch goal with |- ?G => idtac "<infomsg>Goal:" G "</infomsg>" end. +Ltac idtac_context := + try (repeat match goal with H : _ |- _ => revert H end; + idtac_goal; + lazymatch goal with |- ?G => idtac "<infomsg>Context:" G "</infomsg>" end; + fail). |