The Coq mailing list

[Milad Ketabii <ketabii.math AT gmail.com>]

Hi there!

I have a problem, for which a solution already is there. However, I am looking for a better way of accomplishing the task.

Here, I will first explain the problem itself, as much simply as possible. Then I mention the crazy solution which I have. But I hope someone would kindly hint at a superior approach.

The problem and a crazy solution:

I have a formalisation which I intend to break into a base file and some modules, each of which calls this base in.

The base formalisation has variables. These variables are used inside each module as well. We finally would extract executable program into Haskell. 

The base is constituted of some sections. To make the variables in the base file available to the modules (without instantiating them), I have made the out-most part of the base file as a module, rather than a section. This prevents errors that I would get by trying to compile the modules. 

However, the hassle is that I need to put the name of the base module in front of every variable, definition, and function which are celled in the modules. 

Question:

How can I make a base file and call it into the modules which use that base, without being forced to put the name of the base in front of every thing called from the base (and used inside the modules)?

thanks in advance for your help,

Milad