coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Making intros with explict patterns.

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: jean-francois.monin AT imag.fr
Cc: roconnor AT theorem.ca, Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club]Making intros with explict patterns.
Date: Mon, 13 Mar 2006 15:28:53 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Mar 13, 2006 at 12:11:59PM +0100,
jean-francois.monin AT imag.fr
wrote:

> I think you could be satisfied with info intros.

There is also "Show Intros.", but it seems to be buggy. I'm trying
with a fresh SVN trunk checkout and reporting a bug if not fixed.

--
Lionel

[Coq-Club]Making intros with explict patterns., roconnor
- Re: [Coq-Club]Making intros with explict patterns., jean-francois . monin
  - Re: [Coq-Club]Making intros with explict patterns., Lionel Elie Mamane