From 2f667be402bb86e8f79c599ef12072659d19ebe2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 2 Sep 2016 11:40:49 -0700
Subject: Add [idtac_goal]

---
 src/Util/Tactics.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Util/Tactics.v')

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).
-- 
cgit v1.2.3