From 61c1ff3515341b033df9e28fd60664d1a56ef896 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 28 Dec 2002 10:35:12 +0000 Subject: Re-installation nombres dans les motifs sur Z git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zsyntax.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index f05ddeb4c..863e96759 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -70,7 +70,7 @@ Grammar constr constr0 := z_in_com [ "`" znatural:formula($c) "`" ] -> [$c]. Grammar constr pattern := - z_in_pattern [ "`" znatural:number($c) "`" ] -> [$c]. + z_in_pattern [ "`" prim:bigint($c) "`" ] -> [ 'Z: $c ' ]. (* The symbols "`" "`" must be printed just once at the top of the expressions, to avoid printings like |``x` + `y`` < `45`| @@ -234,7 +234,7 @@ Infix "<=" Zle (at level 5, no associativity) : Z_scope. Infix "<" Zlt (at level 5, no associativity) : Z_scope. Infix ">=" Zge (at level 5, no associativity) : Z_scope. Infix ">" Zgt (at level 5, no associativity) : Z_scope. -Infix "?=" Zcompare (at level 5, no associativity) : Z_scope. +Infix "? =" Zcompare (at level 5, no associativity) : Z_scope. Notation "x <= y <= z" := (Zle x y)/\(Zle y z) (at level 5, y at level 4):Z_scope. Notation "x <= y < z" := (Zle x y)/\(Zlt y z) -- cgit v1.2.3