diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 08:03:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 08:03:26 +0000 |
| commit | 9a72107debe9027470c1cc93b869097b3201a967 (patch) | |
| tree | d4a8b1dab605f7984d7466072c2547fdd8c0f159 /theories/Lists | |
| parent | a10a0c02ad7698b778d52d3d0c6093111c24ac43 (diff) | |
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
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/PolyList.v | 8 | ||||
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 9 |
2 files changed, 8 insertions, 9 deletions
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. |