diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 09:01:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 09:01:38 +0000 |
| commit | c076bdf8b80da7de215b26934cc6e9a8d0916837 (patch) | |
| tree | 49eece3e17dcca598dc101554369dfd56234a28c /theories/Init/Peano.v | |
| parent | c85a4e0037cfc5a112e15bce28b4132dbdf3620b (diff) | |
Petites corrections diverses :
- bug d'installation (coq_config.cmo était installé une 2ème fois au
lieu d'installer coq_config.cmx)
- suite nettoyage configure, option reals
- ajout d'une option "only parsing" oubliée dans Peano.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Peano.v')
| -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 b442a8e12..a7e1a39aa 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] *) |