The Coq mailing list

[Taral <taralx AT gmail.com>]

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.

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.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown