The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

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.
> 
> Non, ce n'est malheureusement pas possible. Si vous ecrivez ce bout de
> code (sous la forme d'un "Auto with T1 ... Tn" ou "Auto without T1 ...
> Tn") nous l'integrerons a` la prochaine distribution.

Je vais integrer cela et d'autres fonctionalites sur Auto des que j'ai
un peu de temps libre pour le faire.  Je te tiendrai au courrant Olivier.


Eduardo.