diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-25 12:12:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-25 12:12:47 +0000 |
| commit | dd63c2ac3d144cde87981a9f1bf230dd3b459711 (patch) | |
| tree | bc49954e4d4ef556a39cd44956078efd863f944a /theories/ZArith | |
| parent | d0ee77343eeecae0ad314ea877c60b4dfa77ad41 (diff) | |
Rétablissement affichage des entiers de nat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 28d1c8324..f2f5f3949 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -152,7 +152,7 @@ Syntax constr Zappl_inside [ << (ZEXPR (APPLIST $h ($LIST $t))) >> ] -> [ [<hov 0> "("(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E ")"] ] | Zappl_inject_nat [ << (ZEXPR (APPLIST <<inject_nat>> $n)) >> ] - -> [ [<hov 0> "(inject_nat" [1 1] $n ")"] ] + -> [ [<hov 0> "(inject_nat" [1 1] $n:L ")"] ] | Zappl_inside_tail [ << (ZAPPLINSIDETAIL $h ($LIST $t)) >> ] -> [(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E] | Zappl_inside_one [ << (ZAPPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E] |