coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Liste de hint

From: Olivier PONS <Olivier.Pons AT sophia.inria.fr>
To: coq-club AT pauillac.inria.fr
Subject: Liste de hint
Date: Tue, 27 Jan 1998 11:12:02 +0100

Bonjour,
Peut on modifier momentanement la liste des Hints.
J'aimerais dans certain cas (par exemple quand je deplace du code)
qu' Auto ne puisse momentanement appliquer qu'une liste de theoreme
restreinte puis reprenne son comportement normal.

Olivier

Liste de hint, Olivier PONS
- Re: Liste de hint, Jean-Christophe Filliatre