The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

> I dont understand the following behaviour of Coq (V6.2 beta):
> ...
> Load test1.
> ...
> OK the type list is generalized with A.
> But with a Require, this is no more true:
>
> Why?

When "Variable" is not inside a section, it is equivalent to
"Parameter". So when you compile test1, A is a parameter, and then
when you do "Require test1" you have a parameter A, which will not be
discharged when closing the section because it is not a variable.

When doing "Load test1", it is like an expansion of the contents of
the file test1, and consequently "Variable" is now a real variable,
which will be discharged when closing the section.

> This implies that a  section cannot be  splitted in several modules,
> which is a big problem for me:

Indeed, it is not possible.
A possible solution is to re-instantiate you generalized definitions
in other modules on other variables, like this :

file1 : Section S. 
        Variable A:T.
        Definition foo := ...
        Theorem bar : ...
        ...
        End S.

file2 : Require file1.
        Section S.
        Variable A:T.
        Local foo := (foo A).
        Local bar := (bar A).
        Definition gee := ...
        ...
        End S.

etc.

I don't really know of it is a good solution in practice...

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr