coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Future-proof way of checking that an ltac variable is closed?
Date: Wed, 21 Dec 2016 20:38:31 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f173.google.com
Ironport-phdr: 9a23:IDe7lhKR4ZpiNYfezdmcpTZWNBhigK39O0sv0rFitYgXIv/xwZ3uMQTl6Ol3ixeRBMOAuqkC27Cd6vq6ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaU0cjz2kJLh2MR+erAPLt8BQj5E0eYgrzR6cgHJTfOIe6nlvPknbyxT1/cC284Rk6D8Bk/0k/s9EF679evJrHvRjED06PjVtt4XQvh7ZQF7X6w==

Is there a way to test what the following tactics test in a way that's robust to future changes in Ltac?

Ltac is_closed1 x := let test := constr:(x) in idtac.

Ltac is_closed2 x := match x with _ => idtac end.

Tactic Notation "is_closed3" constr(x) := idtac.

Goal forall (H' : nat -> nat) (H : forall x : nat, x = x), True.

intros H H'.

match goal with

| [ H : forall x, ?P |- _ ]

=> idtac P (* x = x *)

end.

match goal with

| [ H : forall x, ?P |- _ ]

=> is_closed1 P; idtac P (* nat *)

end.

match goal with

| [ H : forall x, ?P |- _ ]

=> is_closed2 P; idtac P (* nat *)

end.

match goal with

| [ H : forall x, ?P |- _ ]

=> is_closed3 P; idtac P (* nat *)

end.

[Coq-Club] Future-proof way of checking that an ltac variable is closed?, Jason Gross, 12/21/2016