coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "St�phane Lescuyer" <lescuyer AT lri.fr>
- To: "Julien Tesson" <julien.tesson AT univ-orleans.fr>
- Cc: "Mailing list Coq" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Module derivation ?
- Date: Mon, 15 Sep 2008 12:23:10 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=I/XmI6UqISYiniBAgW9N6fWP7V02jCnZ9s9+GxX5/mDgTuISwws2PI+MKfhEZ7iNhN e0FLdtK95Tj+fGIaIMJTlYa/z5KU52u2ChrSVUrLBPlLbOX+275jhLcslOTZIqfnsIbZ hkbM5jEmwA6rTTRnycwCfxpRqVxxoX7bL4IOE=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
2008/9/15 Julien Tesson
<julien.tesson AT univ-orleans.fr>:
>
> Is there a way to derive a module from an other one more transparently so
> that I can access C through B1.C ?
If you are using Coq v8.2, there is a new inclusion feature in the
module system that allows you to do exactly what you want:
Module Type B.
...
End B.
Module Type B1.
Include Type B.
Parameter extra_axiom : ...
End B1.
In Coq 8.1 however I dont know of any workaround.
HTH,
Stéphane L.
--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06
- [Coq-Club] Module derivation ?, Julien Tesson
- Re: [Coq-Club] Module derivation ?, Stéphane Lescuyer
- Re: [Coq-Club] Module derivation ?,
Elie Soubiran
- Re: [Coq-Club] Module derivation ?,
Julien Tesson
- Re: [Coq-Club] Module derivation ?, Luke Palmer
- Re: [Coq-Club] Module derivation ?, Luke Palmer
- Re: [Coq-Club] Module derivation ?, Elie Soubiran
- Re: [Coq-Club] Module derivation ?,
Julien Tesson
Archive powered by MhonArc 2.6.16.