The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Here's a somewhat dressed-up version of is_ctor that should run even in 
pre-8.5 versions of Coq (no tactic-in-term).  The ugly control flow 
("fail flailing") due to the absence of tryif is unfortunate, though.

Ltac head_of term :=
  lazymatch term with
  | (?H _) => head_of H
  | _ => term
  end.

Ltac get_value H := eval cbv delta [H] in H.

Ltac is_ctor sym :=
  let H:=fresh in
  let H2:=fresh in
  let A:=fresh in
  try
  (try
   (assert ((forall T, T) -> True) by
    (intro A;
     first [pose sym as H | fail 3 "is_ctor:" sym "is not a valid term"];
     repeat specialize (H (A _));
     pose H as H2;
     first [destruct H | fail 3 "is_ctor:" sym "does not produce an 
inductive type"];
     let C:=get_value H2 in
     let c:=head_of C in
     try (constr_eq c sym; fail 2 (*success*));
     exact I);
    fail 2 "is_ctor:" sym "is not a constructor");
   fail 1 "is_ctor - problem with tactic").

Variable F:nat.
Variable T:Type.
Variable G:T.

Goal True.
Fail is_ctor F.
Fail is_ctor G.
Fail is_ctor X.
is_ctor 0.
Fail is_ctor 1.
is_ctor S.
is_ctor cons.
is_ctor @nil.
is_ctor @eq_refl.
is_ctor true.
is_ctor false.
is_ctor I.
Fail is_ctor (cons 1 nil).
Fail is_ctor True.
Fail is_ctor Type.
exact I.
Qed.

-- Jonathan