Merge PR #195: Complete is_* family of term-examining tactics.

2 files changed, 29 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 15110e701d..fa0e70ba0a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,6 +21,7 @@ Tactics
 - When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
   a locally free identifier anymore. It must use e.g. the "fresh" primitive
   instead (potential source of incompatibilities).
+- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 
 Program
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 57fad85113..845ac67139 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -866,6 +866,34 @@ TACTIC EXTEND is_cofix
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ]
 END;;
 
+TACTIC EXTEND is_ind
+| [ "is_ind" constr(x) ] ->
+  [ match kind_of_term x with
+    | Ind _ -> Proofview.tclUNIT ()
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ]
+END;;
+
+TACTIC EXTEND is_constructor
+| [ "is_constructor" constr(x) ] ->
+  [ match kind_of_term x with
+    | Construct _ -> Proofview.tclUNIT ()
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ]
+END;;
+
+TACTIC EXTEND is_proj
+| [ "is_proj" constr(x) ] ->
+  [ match kind_of_term x with
+    | Proj _ -> Proofview.tclUNIT ()
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ]
+END;;
+
+TACTIC EXTEND is_const
+| [ "is_const" constr(x) ] ->
+  [ match kind_of_term x with
+    | Const _ -> Proofview.tclUNIT ()
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ]
+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