coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Serge Leblanc <serge.leblanc AT wanadoo.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] What is the difference between "Require Import and Require Export"?
- Date: Mon, 25 Jun 2007 07:47:37 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On the page http://cocorico.cs.ru.nl/coqwiki/Require_Import_and_Require_Export
I read the following text:
When the file you are editing is imported, everything in the require export will be imported as well. When the file you are editing is imported, nothing in the require import will be imported as well. But the require import stuff will still be accessable by a fully qualified name.
Unfortunately with this explanation, I doubt that somebody understands !
Cordialy.
|
-- Serge Leblanc gpg --keyserver hkp://subkeys.pgp.net --recv-keys 0x73791C2B Fingerprint: 8E0C 0D6D E026 A278 9278 BF4F 1A93 D552 7379 1C2B |
Attachment:
signature.asc
Description: This is a digitally signed message part
- [Coq-Club] What is the difference between "Require Import and Require Export"?, Serge Leblanc
Archive powered by MhonArc 2.6.16.