coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Finding opaque dependencies

From: Nadeem Abdul Hamid <nadeem AT acm.org>
To: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Finding opaque dependencies
Date: Sat, 7 Mar 2009 22:04:51 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:cc:message-id:from:to:in-reply-to:content-type :content-transfer-encoding:mime-version:subject:date:references :x-mailer; b=UJjua5qx3plmemq4Ux1+TPlGp7Hu6CGAkzY+MKstczQBjTZK5TSE/fG+ZqfcmjYvFf sE38LVVuXdj0ZR02yslmIs5FECEWv43Z1pXUOSLao2SJDZfUxV5Oyxwi9BiDApKAkm6a Q642qXdbPCUPF5eWtY051/avqKQG2JFDRtXHM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Matthieu,

- is there any easy way in general to determine what opaque definitions might have been used?

There's no way to do it yet. We should definitely have a "Print Opaque Dependencies"
to supplement "Print Assumptions". Consider it done!

Wow, thanks! :)

Maybe furthermore, then, to address the second question, it would be nice to have a command like "Redefine Transparent" or something, such that it makes it easier to duplicate an existing opaque definition as transparent and give it a new name. Something like, for example:

Redefine Transparent plus_minus as my_plus_minus.

--- nadeem

[Coq-Club] Finding opaque dependencies, Nadeem Abdul Hamid
- Re: [Coq-Club] Finding opaque dependencies, Matthieu Sozeau
  - Re: [Coq-Club] Finding opaque dependencies, Nadeem Abdul Hamid
  - Re: [Coq-Club] Finding opaque dependencies, Adam Koprowski
    - Re: [Coq-Club] Finding opaque dependencies, Matthieu Sozeau