The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Thu, Mar 19, 2009 at 12:04:19PM -0700, Taral wrote:
> On Thu, Mar 19, 2009 at 10:30 AM, Ian Lynagh 
> <igloo AT earth.li>
>  wrote:
> > consider u:U from n.
> 
> Stop here and look closely:
> 
>   n : N
>   n' : N
>   H1 : g n = Some n'
>   u : U
>   ============================
>    ?1 : g n' = Some (MkN u)
> 
> What's wrong? n is still present! Yet again, a step that bizarrely
> only substitutes into the goal, not the hypotheses. Generating the
> equality is superior to doing the substitutions, again. I think you
> are spending a lot of time trying to work around a fundamental
> brokenness in C-zar.

Is there some subtle reason why C-zar couldn't do what I need it to, or
is it just a matter of waiting for a future release?

Does anyone know if I would have more luck with the development branch?

> P.S. I got this, which made me laugh
> 
> MyLemma < per cases of H':(exists u : U, n = MkN u) by H.
> Anomaly: assert failure
> (file "tactics/decl_proof_instr.ml", line 918, characters 3-9).
> Please report.

Assertion failure? Luxury! I just get segfaults when coq disagrees with
me:

https://logical.saclay.inria.fr/coq-bugs/show_bug.cgi?id=2081
https://logical.saclay.inria.fr/coq-bugs/show_bug.cgi?id=2064

I religiously save before running anything in coqide now...


Thanks
Ian