From fc3f8eb9bcb6645a97a35335d588dbd50231689b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 8 Apr 2008 16:15:23 +0000
Subject: - A little cleanup in Classes/*. Separate standard morphisms on
 relf/sym/trans relations from morphisms on prop connectives and relations. -
 Add general order theory on predicates, instantiated for relations. Derives
 equivalence, implication, conjunction and disjunction as liftings from
 propositional connectives. Can be used for n-ary homogeneous predicates
 thanks to a bit of metaprogramming with lists of types. - Rebind
 Setoid_Theory to use the Equivalence record type instead of declaring an
 isomorphic one. One needs to do "red" after constructor to get the same
 statements when building objects of type Setoid_Theory, so scripts break.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Syntax.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program/Syntax.v')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a518faa570..6158e88f76 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -44,7 +44,7 @@ Implicit Arguments cons [[A]].
 
 Notation " [] " := nil.
 Notation " [ x ] " := (cons x nil).
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1).
 
 (** n-ary exists ! *)
 
-- 
cgit v1.2.3