The Coq mailing list

[Paolo Herms <paolo.herms AT lri.fr>]

I don't think this is a bug.
Ref.Man 2.4.2:
After closing of the section [...] all global objects defined in the section 
are generalized with respect to the variables and local definitions they each 
depended on in the section.
Now, you expect that "C2" depends on "Other" but why should it? As you admit 
the proof, how should Coq know it relies on this hypothesis?
If there were extra local variables or hypothesis in addition to "Other", 
should Coq generalise them, too?
Notice, that you still achieve what you want by generalising explicitly with:

  Proof. generalize Other. admit. Save.

-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Monday 14 November 2011 15:41:23 Victor Porton wrote:
> 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).
> ]]]]