coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Finding opaque dependencies

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>
Cc: Nadeem Abdul Hamid <nadeem AT acm.org>, Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Finding opaque dependencies
Date: Wed, 18 Mar 2009 13:00:19 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=BOUlVNQK2UjRe0bms1kxVI7Yet5Cpyc86M4lC+XO6Xl94JRTC/VzFrKop318i6yJd7 LgRaMRot70eQz2Lg4HbUt8WqQW1Koxjh3T9IBN+Hy2R5ckAqhqYhMv2LPdCIsEeX/P/1 bga9pOrE9xlWTM8iDoRMhWvEIFLYjFW6cb66U=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

�� Hi Matthieu,

On Sun, Mar 8, 2009 at 02:57, Matthieu Sozeau <Matthieu.Sozeau AT lri.fr> wrote:

- 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!

�
�� I'd love to see that future! (figuring "by hand" what opaque definitions are in the way of reduction can be quite painful).

� Adam

--
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[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