The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi,
We are actually thinking about a type-theoretical model of ontologies which uses 
parameterized coercions. However, we get the error "Cannot find the target 
class." with the following Coq code:

Definition Concept := Type.
Definition PrimitiveType : Concept := Type.
Definition RelationType : Concept := Type.

Definition PartOf (A B:PrimitiveType) : RelationType := prod A B.
Definition ContainedIn (A B:PrimitiveType) : RelationType := prod A B.
Definition HasLocation (A B:PrimitiveType) : RelationType := prod A B.

Axiom SR1 : forall (A B:PrimitiveType), ContainedIn A B ->  PartOf A B.
Coercion SR1 : ContainedIn>->  PartOf.

Coercion POL(A B:PrimitiveType)(p:PartOf A B) := fst p. (*<- error *)
Coercion POR(A B:PrimitiveType)(p:PartOf A B) := snd p. (*<- error *)

In fact when I put "A" instead of fst p, it works but it is not the 
semantically expected result. If someone has an idea of how to solve this problem?

Thanks in advance,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard