From d2e15d9a8b3024a09dc298cf143073b4649dce43 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 31 May 2012 22:20:16 +0000
Subject: tactic is_fix, akin to is_evar, is_hyp, is_ ... family

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15406 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cdb192ffa9..599db8365c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -771,6 +771,12 @@ TACTIC EXTEND is_hyp
     | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ]
 END
 
+TACTIC EXTEND is_fix
+| [ "is_fix" constr(x) ] ->
+  [ match kind_of_term x with
+    | Fix _ -> Tacticals.tclIDTAC
+    | _ -> Tacticals.tclFAIL 0 (Pp.str "not a fix 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
-- 
cgit v1.2.3