From aa2f0216bb39a1054737b1edf695f28f59c14ea7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 12 Jun 2014 13:54:41 +0100
Subject: Add an is_cofix tactic

Should we also add is_* tactics for other things?  is_rel, is_meta,
is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const,
is_ind, is_constructor, is_case, is_proj?
---
 tactics/extratactics.ml4 | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c681078fa4..ec120f9c6a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -836,6 +836,13 @@ TACTIC EXTEND is_fix
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ]
 END;;
 
+TACTIC EXTEND is_cofix
+| [ "is_cofix" constr(x) ] ->
+  [ match kind_of_term x with
+    | CoFix _ -> Proofview.tclUNIT ()
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ]
+END;;
+
 (* Command to grab the evars left unresolved at the end of a proof. *)
 (* spiwack: I put it in extratactics because it is somewhat tied with
    the semantics of the LCF-style tactics, hence with the classic tactic
-- 
cgit v1.2.3