diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 28 |
2 files changed, 29 insertions, 0 deletions
@@ -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 |