The Coq mailing list

[Adam Koprowski <koper AT astercity.net>]

  During my work with Coq I quite often encounter message in style of: 
"Anomaly: something. Please report" (very often while working with setoids or 
induction schemas created with Schema command). It's a substantial work to 
report all those errors thus my question: is it really worth doing? I mean is 
there any chance it is going to help with development of stable Coq version?

  Another question. With definitions like:
>  Ltac test1 x := intro x.
>  Ltac test2 x := intros until x.
  and lemma like:
> Theorem everything: forall M, M.
  -) why 'test2 M' fails (No hypothesis x in current goal even after 
head-reduction) while 'intros until M' works fine and 'test1 M' introduces 
hypothesis with name 'M' as expected? This problem was not present in Coq 7.4 as 
far as I know.

   Kind regards,
    Adam Koprowski

--
----------------------------------------------------
-         
akoprow AT cs.vu.nl,
 ICQ: 3204612           -
-  The difference between impossible and possible  -
-      lies in determination (Tommy Lasorda)       -
----------------------------------------------------