coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] assumption after split

From: Marko Malikovi� <marko AT ffri.hr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] assumption after split
Date: Mon, 7 May 2007 13:47:16 +0200 (CEST)
Importance: Normal
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[Coq-Club] assumption after split, Marko Malikovi�
- Re: [Coq-Club] assumption after split, Benjamin Werner
- Re: [Coq-Club] assumption after split, Edsko de Vries
- Re: [Coq-Club] assumption after split, Pierre Casteran