diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 5d3c149ab9..4903d50d17 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -866,6 +866,27 @@ 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;; + (* 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 |