Skip to Content.
Sympa Menu

coq-club - big sections

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

big sections


chronological Thread 
  • From: Loic Pottier <Loic.Pottier AT sophia.inria.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: big sections
  • Date: Wed, 11 Mar 1998 10:06:39 +0100
  • Fax: (33) 93 65 78 58
  • Organization: INRIA, Sophia Antipolis, France
  • Telephone: (33) 93 65 78 19


Hello, 
I dont understand the following behaviour of Coq (V6.2 beta):

First I compile the following file test1.v:
-------------------------
Variable A:Set.

Inductive list:Set:=
  nil:list
  |cons : A -> list -> list.
------------------------
Then I call coqtop:
------------------------
Section test.

Load test1.

End test.

Print list.
>Inductive list [A : Set] : Set :=
      nil : (list A) | cons : A->(list A)->(list A)
-------------------------
OK the type list is generalized with A.
But with a Require, this is no more true:
-------------------------
Section test.

Require Export test1.

End test.

Print list.
>Inductive list : Set :=  nil : list | cons : A->list->list
------------------------------

Why?

This implies that a section cannot be splitted in several modules, which is a 
big problem for me: I have a rather big developpement depending on several 
variables, that I want to use in different instanciations; and then I have to 
write it in a single big file. For every modification , addition to this 
file, 
I must load it, which is very slow...

In fact I would like to be able to split my file into several small modules, 
variables being declared into the first module, and then generalize all files 
into a single section:

Section generalize.
Require Export file1.
...
Require Export filen.
End generalize.

Loic











Archive powered by MhonArc 2.6.16.

Top of Page