The Coq mailing list

[Loic Pottier <Loic.Pottier AT sophia.inria.fr>]

 Dans le message 
<199803110921.KAA22179 AT pc85.lri.fr>,
 
  du Wed, 11 Mar 1998 10:21:33 +0100, 
  Jean-Christophe Filliatre ecrit:
   >
   >> 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...
It is a solution, but very heavy if you have 20 variables...More, you have to 
unfold everything in proofs.
Now my question is "why is it necessary to change variables into parameters 
at 
global level in compilation?".

Loic