From f81e9e599f6003f164307ab31edce91a125517e2 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 24 Nov 2002 23:50:51 +0000 Subject: Traitement des parenthèses de nat au niveau du printer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3273 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zsyntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/ZArith/Zsyntax.v') 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))) >> ] -> [ [ "("(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E ")"] ] | Zappl_inject_nat [ << (ZEXPR (APPLIST <> $n)) >> ] - -> [ [ "(inject_nat" [1 1] "(" $n "))"] ] + -> [ [ "(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] -- cgit v1.2.3