coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
- To: Olivier PONS <Olivier.Pons AT sophia.inria.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: Liste de hint
- Date: Tue, 27 Jan 1998 11:22:12 +0100
> 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.
Non, ce n'est malheureusement pas possible. Si vous écrivez ce bout de
code (sous la forme d'un "Auto with T1 ... Tn" ou "Auto without T1 ...
Tn") nous l'intègrerons à la prochaine distribution.
--
Jean-Christophe FILLIATRE
- Liste de hint, Olivier PONS
- Re: Liste de hint, Jean-Christophe Filliatre
Archive powered by MhonArc 2.6.16.