diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-15 15:25:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-15 15:25:15 +0000 |
| commit | 5f5eddc1779ccb0afd022d4b54ae6405d0439488 (patch) | |
| tree | b351b728c03bc168a031c4bf1a9d02df066390d9 /theories/QArith | |
| parent | d8070414d12db4db35f7b75b2b102ec1d0cfe679 (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/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 9ebfa19cb..f4b57d5be 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -31,7 +31,7 @@ Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. Arguments Scope inject_Z [Z_scope]. -Notation " 'QDen' p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope. +Notation QDen p := (Zpos (Qden p)). Notation " 0 " := (0#1) : Q_scope. Notation " 1 " := (1#1) : Q_scope. |