diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Peano.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index b442a8e125..a7e1a39aa2 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -125,8 +125,8 @@ Qed. (** Standard associated names *) -Notation plus_0_r_reverse := plus_n_O. -Notation plus_succ_r_reverse := plus_n_Sm. +Notation plus_0_r_reverse := plus_n_O (only parsing). +Notation plus_succ_r_reverse := plus_n_Sm (only parsing). (** Multiplication *) @@ -156,8 +156,8 @@ Hint Resolve mult_n_Sm: core v62. (** Standard associated names *) -Notation mult_0_r_reverse := mult_n_O. -Notation mult_succ_r_reverse := mult_n_Sm. +Notation mult_0_r_reverse := mult_n_O (only parsing). +Notation mult_succ_r_reverse := mult_n_Sm (only parsing). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) |