The Coq mailing list

[Benedikt Ahrens <Benedikt.Ahrens AT unice.fr>]

On 11/11/2011 11:04 PM, Victor Porton wrote:
> The following:
> 
> [[[[
> Section sect.
> 
>   Theorem C2: (2+2=4).
> (*Proof. tauto. Qed.*)
>   proof.
>     thus thesis.
>   end proof.
> 
> End sect.
> ]]]]
> 
> produces the error:
> 
> Error: Proof editing in progress.
> Proofs currently edited: C2.
> 
> Interestingly it does not work only with a structured proof (proof...end 
> proof) and produces no error with plain tactics proof (Proof. tauto. Qed.). 
> It also works if we remove Section.
> 
> Does this mean that structured proof don't work inside sections?

No, it simply means that "end proof." does not eliminate the need for
proofs to be saved using "Qed." or "Defined.".

Try, outside any section,

  Theorem C2: (2+2=4).
  proof.
    thus thesis.
  end proof.
Check C2.

and you'll notice that sections don't have anything to do with it. In
your case it was merely the first thing that triggered the symptom of
your proof not being saved.

benedikt