2.5 Section mechanism

2.5 Section mechanism

The sectioning mechanism allows to organize a proof in structured sections. Then local declarations become available (see section 1.3.2).

2.5.1 Section ident

This command is used to open a section named ident.


Variants:
  1. Chapter ident
    Same as Section ident

2.5.2 End ident

This command closes the section named ident. When a section is closed, all local declarations are discharged. This means that all global objects defined in the section are closed (in the sense of l-calculus) with as many abstractions as there were local declarations in the section explicitly occurring in the term. A local object in the section is not exported and its value will be substituted in the other definitions.

Here is an example :
Coq < Section s1.

Coq < Variables x,y : nat.
x is assumed
y is assumed

Coq < Local y' := y.
y' is defined

Coq < Definition x' := (S x).
x' is defined

Coq < Print x'.
x' = (S x)
     : nat

Coq < End s1.
[Cooking #x'.cci]
[Cooking #x'.fw]
Constant x' : nat->nat

Coq < Print x'.
x' = [x:nat](S x)
     : nat->nat
Note the difference between the value of x' inside section s1 and outside.


Error messages:
  1. Section ident does not exist (or is already closed)
  2. Section ident is not the innermost section



Remarks:
  1. Some commands such as Hint ident or Syntactic Definition which appear inside a section are cancelled when the section is closed.
  2. Usually, all identifiers must be distinct. However, a name already used in a closed section (see 2.5) can be reused. In this case, the old name is no longer accessible.
  3. A module implicitly open a section. Be careful not to name a module with an identifier already used in the module (see 5.4).


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.0.1.4.html at 8/10/98