The Coq mailing list

[Loic Pottier <loic.pottier AT sophia.inria.fr>]

Hi,
I have the following problem with universes and type classes (?):

Class Qs(E :Type)(F:Type)(P:E ->Prop)(A:F):= {qsprop: Prop}.
Notation "'for_all' x 'in' A , P " :=
  (@qsprop _ _ (fun x => P) A _) (right associativity, at level 200, x 
ident).

Instance qsprop1(E:Type)(P:E ->Prop):Qs E _ P E:= {qsprop := forall x:E, 
P x}.

Definition empty{E:Type} := fun x:E => False.

Goal for_all E in Type, for_all x in E, not (empty x).
intro E.
intro x.
intro.
apply H.
Qed.
Error: Universe inconsistency.

but with (@empty E x), it works!

Loïc