From 2c082f731f1fb6c867908504c4e454119e58e593 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 16 Jun 2016 07:39:43 -0400
Subject: Add is_const

---
 ltac/extratactics.ml4 | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 4903d50d17..97d33fb7ab 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -887,6 +887,13 @@ TACTIC EXTEND is_proj
     | _ -> 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
-- 
cgit v1.2.3