aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/intro.tex
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-15 15:25:15 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-15 15:25:15 +0000
commit5f5eddc1779ccb0afd022d4b54ae6405d0439488 (patch)
treeb351b728c03bc168a031c4bf1a9d02df066390d9 /theories/Logic/intro.tex
parentd8070414d12db4db35f7b75b2b102ec1d0cfe679 (diff)
Autour du parsing:
- Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/intro.tex')
0 files changed, 0 insertions, 0 deletions