coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- big sections, Loic Pottier
- Re: big sections, Jean-Christophe Filliatre
- <Possible follow-ups>
- Re: big sections,
Loic Pottier
- Re: big sections, Bruno Barras
- Re: big sections, Hugo Herbelin
Archive powered by MhonArc 2.6.16.