diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:50:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:50:51 +0000 |
| commit | f81e9e599f6003f164307ab31edce91a125517e2 (patch) | |
| tree | 61b6762d9393c928388f59fbcba6822f80ad734b /theories/ZArith/Zsyntax.v | |
| parent | 55a483ea0694eab627e9386f69f3c05693e37fa1 (diff) | |
Traitement des parenthèses de nat au niveau du printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zsyntax.v')
| -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 760c1fc89..28d1c8324 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 ")"] ] | Zappl_inside_tail [ << (ZAPPLINSIDETAIL $h ($LIST $t)) >> ] -> [(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E] | Zappl_inside_one [ << (ZAPPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E] |