The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Thu, Mar 10, 2011 at 8:17 PM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> Le jeudi 10 mars 2011 à 19:56 +0100, Stéphane Lescuyer a écrit :
> Unfortunately, this approach turns out to be unpractical on the actual
> code where theorems are more complicated. Indeed, it requires all the
> preceding arguments (including unrelated ones!) to be implicit and
> maximally inserted too, just to be sure Coq doesn't stop prematurely
> from inserting evars. Unfortunately, some of them cannot be inferred
> automatically in most cases and have to be specified, so the user is
> forced to use a cumbersome syntax (either @... or (...:=...)), which
> defeats the whole point.

I encountered this issue once in a development and the best thing I
could think of was to use the 'Proof with' facility. Start your proof
with

Proof with (eauto with typeclass_instances).

and end all your "apply" tactics with "...". It's not very aesthetic
but is saves typing, and that also serves as a syntactic reminder that
there's something non trivial going on under the hood.

Stéphane


-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06