diff options
author | 2016-06-16 07:39:43 -0400 | |
---|---|---|
committer | 2016-06-16 07:39:43 -0400 | |
commit | 2c082f731f1fb6c867908504c4e454119e58e593 (patch) | |
tree | 625acd069f9a9f2550e8af6863ce28cc3afe8785 | |
parent | 3eb1e805be574064225e832bffb01f2410c41518 (diff) |
Add is_const
-rw-r--r-- | ltac/extratactics.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 4903d50d1..97d33fb7a 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 |