coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER <Cedric.Auger AT lri.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] matching variables in Ltac
- Date: Wed, 05 May 2010 12:55:25 +0200
- Organization: ProVal
Le Wed, 05 May 2010 11:49:30 +0200, Loic Pottier <loic.pottier AT sophia.inria.fr> a écrit:
Hi,
with Ltac, can we match names of variables in a pattern, to use them in right-hand side? e.g:
Ltac tac:=
match goal with
|- forall ?x:?E, ?P => idtac x
end.
(but this does not work :-( )
or, if not, associate a character to a type so that intro will use it by default?
Loïc
I think it is not satisfactory, but you can do something like:
Ltac tac:=
let x := fresh "forced_var" in
intro x; revert x; idtac x.
Goal forall P, P /\ False.
tac.
It will change the name of your binder so you can chose it.
To get the name of your binder, it seems to require either an extension of the match rule, either to make your own tactic in caml.
the intro tactic is defined in [trunk]/tactics/tactics.mli
There is a function called find_intro_names of signature:
val find_intro_names : rel_context -> goal sigma -> identifier list
so your function should look like:
let print_universal_first_binder ctx gl =
match Tactics.find_intro_names ctx gl with
| [] -> tclFAIL
| id::_ -> tclIDTAC_MESSAGE (Pp.str (Names.string_of_id id))
I am not sure of the result as I have never written plugins/tactics in Ocaml
--
Cédric AUGER
Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
- [Coq-Club] matching variables in Ltac, Loic Pottier
- Re: [Coq-Club] matching variables in Ltac, Paolo Herms
- Re: [Coq-Club] matching variables in Ltac, AUGER
- <Possible follow-ups>
- Re: [Coq-Club] matching variables in Ltac, Arthur Charguéraud
Archive powered by MhonArc 2.6.16.