The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

 Hi all,
I found a coq feature which doesn't seem natural:

Create 3 files:

-------------------------------------------
(*base.v*)
Record A :=
{ S: Type;
  Eq: S -> S -> Prop
}.

Record B :=
{ S': Type;
  Eq': S' -> S' -> Prop
}.
-------------------------------------------
(*baseA.v*)
Require base.

Definition As :=
{| base.S' := base.A;
   base.Eq' := fun a b => a = b
|}.
-------------------------------------------
(*baseB.v*)
Require base.

Definition Bs :=
{| base.S := base.B;
   base.Eq := fun a b => a = b
|}.
-------------------------------------------
(*baseC.v*)
Require baseA.
Require baseB.
-------------------------------------------
compile all:

coqc base.v; coqc baseA.v; coqc baseB.v

and then try to compile baseC.v, it will fail
 (hopefully, since we morally defined the set of all sets),
 but when we are used to functionnal programing, we don't expect
 such an error, as something compiled can always be used...

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay