The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 29 Jan 2013 20:01:49 +0100,
Gabriel Scherer 
<gabriel.scherer AT gmail.com>
 a écrit :

> (Granted, the way OCaml collect backtraces does not ease proper
> backtrace preservation, but I have no bright idea for a solution that
> would incur no additional cost and make everyone happier than with the
> current situation.)

I guess I would be ready to pay an additional cost for having a cleaner
Coq code, and better error reporting system. Although it has little to
do with that matter, I would be glad to get rid of all side effects of
the Coq interpreter (well, maybe not all, but at least, I would like
that an Undo reverts Coq back to its previous state [ie. including
universe levels and evars numbering]). I think it is not that much
difficult to store an history of pairs (max used existential variable,
max used universe name) which would be restored when running Undo
command.