coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with Modules

From: "Elie Soubiran" <soubiran AT lix.polytechnique.fr>
To: Robert <robdockins AT fastmail.fm>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Problem with Modules
Date: Mon, 2 Jul 2007 16:56:16 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:references:x-google-sender-auth; b=diRCZe3YpDpuLWVr6GXYirM7T44IcXxIciv3d5TMMIZFbPBb0X8is4FjVnBVcSh1cyY7o8MDKavNHFJwuiHFu2tfnM7zcSdnAD0eeP8OVSj3FMp0wKrD0jRAreIbliR6KK9ydgHioTEXpaEVn+917qgEU8o3Bb9Y/ABnzyekz3g=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello Robert,

This problem is due to a bad interaction between
opacity of definition ( when we use Qed) and subtyping.

Replace Qed by Defined in your Lemma Extension and it will work.

Elie.

On 6/28/07, Robert <robdockins AT fastmail.fm> wrote:

I'm trying to migrate a small proof I've done to use modules because I
think
it will make things easier in the long run.   However, I'm running into
a
problem that I don't know how to solve.  Coq is complaining when I try
to
form certain kinds of modules, claiming
   "Signature components for label ... do not match"

I've attached a short proof script that demonstrates the problem for me.
Is
this a bug or is there some subtlety of module type-checking that I have
missed?

coqcop reports
  "Welcome to Coq 8.1 (Feb. 2007)"

Many Thanks
Rob Dockins
--
  Robert
  robdockins AT fastmail.fm

Re: [Coq-Club] Problem with Modules, Elie Soubiran