From 22cc653ceff98ea69d0975ee0ccdcecc4ba96058 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 28 Mar 2008 20:40:35 +0000
Subject: Improve error handling and messages for typeclasses. Add definitions
 of relational algebra in Classes/RelationClasses including equivalence,
 inclusion, conjunction and disjunction. Add PartialOrder class and show that
 we have a partial order on relations. Change SubRelation to subrelation for
 consistency with the standard library. The caracterization of PartialOrder is
 a bit original: we require an equivalence and a preorder so that the
 equivalence relation is equivalent to the conjunction of the order relation
 and its inverse. We can derive antisymmetry and appropriate morphism
 instances from this. Also add a fully general heterogeneous definition of
 respectful from which we can build the non-dependent respectful combinator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/dependentind.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 8b8ce00987..be7b77ef00 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -35,7 +35,7 @@ Inductive ctx : Type :=
 | empty : ctx
 | snoc : ctx -> type -> ctx.
 
-Notation " Γ , τ " := (snoc Γ τ) (at level 20, t at next level).
+Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
 
 Fixpoint conc (Γ Δ : ctx) : ctx :=
   match Δ with
@@ -43,7 +43,7 @@ Fixpoint conc (Γ Δ : ctx) : ctx :=
     | snoc Δ' x => snoc (conc Γ Δ') x
   end.
 
-Notation " Γ ; Δ " := (conc Γ Δ) (at level 20).
+Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity).
 
 Inductive term : ctx -> type -> Type :=
 | ax : forall Γ τ, term (Γ, τ) τ
-- 
cgit v1.2.3