coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Intros

From: Jeffrey Terrell <jeff AT kc.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Intros
Date: Mon, 06 Sep 2010 20:57:57 +0100

Dear Coq Club,

I'd be grateful if someone could tell me why

Definition P : Prop := True -> True -> True.
Goal P.
intro.

unfolds P (and adds True to the context) whereas

Definition P : Prop := True -> True -> True.
Goal P.
intros.

doesn't. Thanks.

Regards,
Jeff.

[Coq-Club] Intros, Jeffrey Terrell
- Re: [Coq-Club] Intros, Adam Chlipala
  - RE: [Coq-Club] Intros, Georges Gonthier