tac_wit_ref.v « success « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/success/tac_wit_ref.v

blob: 8bde31858e0d7b86db0ac5af25633b28852cef35 (plain)

Tactic Notation "foo" reference(n) := idtac n.

Goal forall n : nat, n = 0.
Proof.
intros n.
foo nat.
foo n.
Abort.