diff options
| author | herbelin | 2002-04-17 11:49:07 +0000 |
|---|---|---|
| committer | herbelin | 2002-04-17 11:49:07 +0000 |
| commit | cda6963b3ca8fd75c00a0c65dd9ecffdeadfb3c3 (patch) | |
| tree | 453dbe7cc01abe5aa6413076365ad00576654572 /theories/ZArith/Zsyntax.v | |
| parent | 4bdc6a6515de45027e43ad79271cf2d8793394e4 (diff) | |
Quelques bugs avec inject_nat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 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 c68c9b218a..fd134f2df3 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -157,7 +157,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] |