coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Modules and Hints

From: "Elie Soubiran" <soubiran AT lix.polytechnique.fr>
To: "Brian E. Aydemir" <baydemir AT cis.upenn.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Modules and Hints
Date: Wed, 28 Mar 2007 15:46:36 +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=cQUGMS9/2teMNconIc3Ao12VYDvhp7Wbp0ZR3jVC93EAKl4A973S0+PFJHnCasFVusK6IUdvO2A1xfckrsMCHIej5OZdeN5uo+3ZC6ezJ4+zKqI46mHeg6S6hrSgBdovL3+UFYI+L2z7LjpVNF7jw2nguZK9iOmrIewq5N3893A=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello Brian,

At the page 174 of the refman (subsection 8.13.5),

"all hints of a module A that are not defined inside a section
(and not defined with option Local) become available when
the module A is imported (using e.g. Require Import A.)."

But i think it speaks about importing a module that is not present
in your current environment.

[1] Suppose that I'm not allowed to change FOO. Is there some way I
could have declared Foo such that P_true would _not_ end up in the
Hints database.

You can do :

Module Foo <: FOO.
Parameter P : nat -> Prop.
Axiom P_true : forall n, P n.
End Foo.

[2] Is the behavior I'm seeing actually the intended behavior?

In my opinion it is the good behavior. Before you closed Foo the core database
contains "apply P_true" and after you closed Foo it contains "apply Foo.P_true".

We should take this as an extension of (module's) localisation to non-logical object.

I hope it will help.

Elie

[Coq-Club]Modules and Hints, Brian E. Aydemir
- Re: [Coq-Club]Modules and Hints, Elie Soubiran