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

1 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 8b8ce0098..be7b77ef0 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 (Γ, τ) τ