Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct


Chronological Thread 
  • From: Emile Lunardon <emile.lunardon AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
  • Date: Sun, 25 Jan 2015 05:51:48 +0100

UNSUBSCRIBE

2015-01-24 16:33 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:

On 01/24/2015 03:11 AM, Jason Gross wrote:
Hi,

In case others may find this discovery interesting (if you have not already
made it yourselves):
It is possible to mostly eliminate the verbose [match goal with ... end]
construct in trunk/8.5 by using the following tactic:

   Ltac hyp := multimatch goal with H : _ |- _ => constr:H end.

Note that [let H := hyp in ... ] will automatically backtrack across
failures of subsequent tactics, due to [multimatch]:

   Goal False -> True -> False -> True.
     intros.
     let H := hyp in exact H.

Using open_constr and uconstr tactic notations, I presume the other
features of match (pattern matching on the body and the type) can be
duplicated with shorter syntax, too.

-Jason


I wasn't able to duplicate the match feature of named pattern variables with any combo of open_constr and uconstr, at least not without using evars in their place (which is not as good as one can easily leave unsolved evars as a result).

Which is one reason why I was asking you about those other Tactic arg notations that are undocumented.

-- Jonathan





Archive powered by MHonArc 2.6.18.

Top of Page