aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/PolyListSyntax.v
diff options
context:
space:
mode:
authorfilliatr2000-06-21 01:11:51 +0000
committerfilliatr2000-06-21 01:11:51 +0000
commit0940e93d753c2df977e44d40f5b9d9652e881def (patch)
tree918eaeeae94c5875ee45d2bead6b7cd91f09e9f2 /theories/Lists/PolyListSyntax.v
parente7c6f94b15d15dbf0d15f08982f04076abdd0fa7 (diff)
theories/Lists
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/PolyListSyntax.v')
-rw-r--r--theories/Lists/PolyListSyntax.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
new file mode 100644
index 0000000000..a19a3dcc14
--- /dev/null
+++ b/theories/Lists/PolyListSyntax.v
@@ -0,0 +1,7 @@
+
+(* $Id$ *)
+
+(* Syntax for list concatenation *)
+Require PolyList.
+
+Infix RIGHTA 7 "^" app.