The Coq mailing list

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

Hi,
With the following code fragment:
(* Basic universes *)
Definition Universal                        := Type.
Definition Concept              : Universal := Type.
Definition Association          : Universal := Type.
Definition OntoType(c:Type)                 := Type.
Definition OntoDomain(c:Type)               := Type.

Parameter Relation :  (OntoType Concept) -> (OntoType Concept) -> Prop.

Structure PT    : OntoType Concept   := {}.
Structure PD    : OntoType PT        := {PDsub   :> PT}.
Structure ED    : OntoType PT        := {EDsub   :> PT}.
Structure AB    : OntoType PT        := {ABsub   :> PT}.
Structure R     : OntoType AB        := {Rsub    :> AB}.
...

Class RelOnto (X Y:OntoType Concept) : Association := { RelOnto_prop : 
Relation X Y}.

Class Reflexive  : Prop :=
           Reflexivity : forall X:OntoType Concept, Relation X X.

Class Irreflexive  : Prop :=
          Irreflexivity : forall (X Y:OntoType Concept), ~Relation X X.

Class Antisymmetric : Prop :=
          Antisymmetry : forall (X Y :OntoType Concept), Relation X Y 
-> Relation Y X -> X = Y.

Class Asymmetric : Prop := {
           Asym_Irr   :> Irreflexive ;
           Asym_Anti  :> Antisymmetric}.

Class Transitive  : Prop :=
           Transitivity : forall X Y Z:OntoType Concept, Relation X Y 
-> Relation Y Z -> Relation X Z.

Class POR  : Prop := {
           POR_R    :> Reflexive ;
           POR_AS   :> Antisymmetric ;
           POR_T    :> Transitive }.

Class PartOf {X Y:OntoType Concept} : Prop := {
           PartOf_s      :> RelOnto X Y;
           PartOf_p      :> POR }.
============================================
I got the following error:
"Anomaly: Uncaught exception Option.IsNone. Please report.Compilation 
output:
File "C:\Users\Richard\Desktop\Documents\Coq-programs/JLComp1.v", line 
73, characters 0-123:

Anomaly: Uncaught exception Option.IsNone. Please report."
If anyone has an explanation...
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