diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-28 10:35:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-28 10:35:12 +0000 |
| commit | 61c1ff3515341b033df9e28fd60664d1a56ef896 (patch) | |
| tree | f49dd9f5186ad914c613043d830f1bb609a137bd | |
| parent | c4a45cc04f9c350c38b148a85bed0c7e88ca5afc (diff) | |
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
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 4 |
1 files 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) |