From c076bdf8b80da7de215b26934cc6e9a8d0916837 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 2 Jun 2008 09:01:38 +0000
Subject: 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
---
 Makefile.build        | 2 +-
 configure             | 3 +--
 theories/Init/Peano.v | 8 ++++----
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 23fdf24cda..8a6bf2df4e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -657,7 +657,7 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)/states
 	cp states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
-	cp $(LINKCMO) $(LINKCMOCMXA) $(GRAMMARCMA) $(FULLCOQLIB)
+	cp $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
 
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
diff --git a/configure b/configure
index 7e31a1f1b0..a23a5bfac8 100755
--- a/configure
+++ b/configure
@@ -127,8 +127,7 @@ while : ; do
     -prefix|--prefix) prefix_spec=yes
                       prefix="$2"
 		      shift;;
-    -local|--local) local=true
-		    reals=all;;
+    -local|--local) local=true;;
     -src|--src) src_spec=yes
                 COQSRC="$2"
 	        shift;;
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] *)
 
-- 
cgit v1.2.3