The Coq mailing list

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

I don't see what is the problem with assert, "assert (H : P)" is
basically "cut P" with the goals generated the other way, so it is
exactly what you asked for in your first message ; in particular, it
does add an hypothesis named H of type P in the second goal.
Note that assert can be used as pose as well : "assert (H := t)" will
act as "pose (H := t); clearbody H".

HTH,

Stéphane

On Tue, Apr 6, 2010 at 1:22 PM, andré hirschowitz 
<ah AT unice.fr>
 wrote:
> no, if I experiment correctly.
>
> assert generates two goals and does not forward to the second one the
> formula produced for the first one.
>
> Thanks for your answer.
>
> ah
>
>>
>>
>> I think you are looking for the following?
>>
>>  assert (myname : mytype).
>>
>>
>
>



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