The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

It is because the tactic after the semicolon is applied to all the
subgoal generated by the tactic before the semicolon.

Here there is no assumption B corresponding to the second
subgoal generated by split.

Benjamin

Le 7 mai 07 à 13:47, Marko Maliković a écrit :

> 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,
>
> Marko Maliković
> Faculty of Arts and Sciences in Rijeka, Croatia
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club