The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The last line of this file does not compile. What is my error?

[[[[
Hypothesis P: nat->Prop.
Hypothesis Q: nat->Prop.

Axiom Eq: forall x:nat, P(x)<->Q(x).

Class C := {
  num: nat;
  cond: P num
}.

Section sect.
  Hypothesis Other: forall obj:C, Q num.

  Instance C2: C := { num:=0 }.
  Proof. Admitted.
End sect.

Axiom ax2: forall obj:C, Q num.

Definition C3 := C2(ax2).
]]]]

-- 
Victor Porton - http://portonvictor.org