diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index cdb192ffa9..599db8365c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -771,6 +771,12 @@ TACTIC EXTEND is_hyp | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ] END +TACTIC EXTEND is_fix +| [ "is_fix" constr(x) ] -> + [ match kind_of_term x with + | Fix _ -> Tacticals.tclIDTAC + | _ -> Tacticals.tclFAIL 0 (Pp.str "not a fix 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 |