diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c681078fa4..ec120f9c6a 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -836,6 +836,13 @@ TACTIC EXTEND is_fix | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] END;; +TACTIC EXTEND is_cofix +| [ "is_cofix" constr(x) ] -> + [ match kind_of_term x with + | CoFix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] +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 |