From 9a72107debe9027470c1cc93b869097b3201a967 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 10 Oct 2003 08:03:26 +0000
Subject: Renommage en v8 de PolyList en List et List en MonoList

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/PolyList.v       | 8 ++++++++
 theories/Lists/PolyListSyntax.v | 9 ---------
 2 files changed, 8 insertions(+), 9 deletions(-)

(limited to 'theories/Lists')

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 681e0cb1c..450fedfc6 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -631,3 +631,11 @@ Reflexivity.
 Qed.
 
 End Functions_on_lists.
+
+(** Exporting list notations *)
+
+V8Infix "::" cons (at level 45, right associativity) : list_scope.
+
+Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++".
+
+Open Scope list_scope.
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
index 640cf3fbf..a4b6a57aa 100644
--- a/theories/Lists/PolyListSyntax.v
+++ b/theories/Lists/PolyListSyntax.v
@@ -8,12 +8,3 @@
 
 (*i $Id$ i*)
 
-(** Syntax for list concatenation *)
-
-Require PolyList.
-
-V8Infix "::" cons (at level 45, right associativity) : list_scope.
-
-Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++".
-
-Open Scope list_scope.
-- 
cgit v1.2.3