The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 When developping some large proof segmented in sections, I met the 
following scheme.

Section S.
 Hypothesis H : P.

Lemma difficult_lemma : Q.
Admitted. (* But I presume that H is used in this proof *)

Theorem corollary : R.
 Proof.
   ... apply difficult_lemma.
Qed.

End S.

Since there is no proof term for the lemma, if the corollary doesn't apply
directly H, the discharging mechanism makes the type of corollary
being R (and not P -> R). That means that all the development after S's
closing will be inconsistent when I (at least) prove the lemma.

Is there a simple way to deal with this problem?

Thanks,

Pierre