diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-10 15:27:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-10 15:27:38 +0000 |
| commit | 19b041bcc069e79608392d705fa9998440d50815 (patch) | |
| tree | ade8280a18fdb435ff6efcba4312cfa6ad3fb7e7 /library/lib.mli | |
| parent | 3dc64aa7b1d8e2d7388b5386cd3bc4387498c216 (diff) | |
Amélioration de la colorisation, du backtrack et des messages de CoqIDE
- Colorisation:
- on ne colorie que les noms de commandes que si en début de phrase
(par exemple: Definition F := fun Local => Local) ne colorie pas
Local),
- ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset
sont uniformément mis en valeur).
- Backtracking: résolution bug #1538 et réactivation de la possibilité de
déclarer des défs, types, etc pendant une session de preuve. En revanche,
il n'est pas clair que cela fonctionne bien avec le mode déclaratif.
- Messages d'erreur : on ne capture la sortie de coq qu'après
l'initialisation pour que les erreurs d'initialisation soit
affichées (cf bug #1424 and item 5 of #1123).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions