The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 01, 2014 at 04:28:44PM -0400, Jonathan wrote:
> Goal mytype.
> econstructor.
> 
> produces the goal like:
> 
> 1 subgoals
> , subgoal 1 (ID 4)
> 
>   ============================
>    P ?3

Sure, but I don't see why you can't prove as a forward step (pt := P t)
and applt (Mytype pt), or just apply (@Mytype t).
Is t so horrible that you cannot construct it by hand?

I feel so naive, but I don't get if it is actually necessary to play
with evars this way or it just that people find it convenient.

I have some examples where one really needs an evar floating around, but
this one does not seem of that kind (I' thinking at the big enough library
by Cyril Cohen, or at the [: ] patterns of ssr to spill subproofs).

Thanks for the patience,
-- 
Enrico Tassi