The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

You forgot to give a parameter of type Set to your my_trans2.

Here is a version that compiles. Note the "About" commands that give
you the type and implicit arguments of your identifiers.
The parameter "set" is given to my_trans2 through the "Generalizable  
Variables"
command.

It is also possible to give it explicitely.

Pierre




Class Relation {set: Set} := {
}.

About Build_Relation.

Implicit Arguments Build_Relation [set].

About Build_Relation.


Definition compose_relation_classes {set:Set} (f g: @Relation set) :
  @Relation set :=
  Build_Relation  .

About compose_relation_classes.


Generalizable Variables set.
Definition my_trans2 `(r: Relation ) := compose_relation_classes  r r = r.






Quoting Victor Porton 
<porton AT narod.ru>:

> Why this does not compile?
>
> [[[
> Class Relation {set: Set} := {
> }.
>
> Definition compose_relation_classes {set:Set} (f g: @Relation set) :=
>   Build_Relation.
>
> Definition my_trans2(r: Relation) := compose_relation_classes r r = r.
> ]]]
>
> --
> Victor Porton - http://portonvictor.org