The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT students.cs.unibo.it>]

On Fri, Sep 24, 1999 at 14:52:13 +0200, Frederic Blanqui wrote:
> > I get
> > 
> > Uncaught exception: File "equality.ml", line 0, characters 20213-20225:
> > Assertion failed
> > If this is in user-written tactic code, then it needs to be modified.
> > If this is in system code, then
> > it needs to be reported.
> 
> I think it is due to the fact that the tactics Discriminate or Injection
> have been defined on = and not on ==.

 I was almost convinced when I saw this, i.e. a theorem that could be
 proved but whose instances could not:


 Inductive T : Type :=  atom : (T':Type)T'->T.

 Theorem ok :
   (T':Type; T'':Type; t':T' ; t'':T'') ~T'==T''->~(atom T' t')==(atom T'' 
t'').
 Unfold not; Intros; Apply H; Inversion H0; Reflexivity.
 Qed.

 Theorem instance_of_ok :
   ~nat==bool->~(atom nat O)==(atom bool true).
 Unfold not; Intros; Apply H; Inversion H0.

 Error during interpretation of command:
 Unfold not; Intros; Apply H; Inversion H0.
 Uncaught exception: File "equality.ml", line 0, characters 20213-20225: 
Assertion failed
 If this is in user-written tactic code, then it needs to be modified.
 If this is in system code, then
 it needs to be reported.


                                                        Hi,
                                                        C.S.C.

-- 
-----------------------------------------
Real Name: Claudio Sacerdoti Coen
Address: via del Colle n.6
         S. Lazzaro di Savena (BO)
         Italy
e-mail:  
sacerdot AT cs.unibo.it
-----------------------------------------