The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Mon, May 07, 2007 at 01:47:16PM +0200, Marko Malikovi? wrote:
> Greetings for everybody,
> 
> I'm new in Coq. Please, can somebody explain to me this error:
> 
> Coq < Section Proba.
> 
> Coq < Variable A B:Prop.
> A is assumed
> B is assumed
> 
> Coq < Hypothesis H:A.
> H is assumed
> 
> Coq < Goal A /\ B.
> 1 subgoal
> 
>   A : Prop
>   B : Prop
>   H : A
>   ============================
>    A /\ B
> 
> Unnamed_thm < split;assumption.
> Toplevel input, characters 6-16
> > split;assumption.
> >       ^^^^^^^^^^
> User error: No such assumption
> 
> Thank you very much,

After split, you need to prove A and B, but only A is an assumption (B is 
not).

If you add another hypothesis H':B, it should work.

Edsko