coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The dependency graphs of Coq theorems

From: Hai WAN <wan.whyhigh AT gmail.com>
To: Coq Club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] The dependency graphs of Coq theorems
Date: Thu, 26 Feb 2009 09:47:27 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=w+MSXoiRs2n+WtfjlAV2yW53rHh5u70onhRBSHSScl62Hk10WpyX4ddLdn9leZ/DY8 6eFY137F/nnql6ELJsA2L5hCZvtLKZG9x+U+7CxO61WQK+j3pKAOwgJgdbsmeIo0+QnU 6hX4aOhxdCc4UKaaMiG/aljSy2npPiXJ8P5ts=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

Is there any commands can help me to explore the dependencies among theorems in a Coq proof script?

I've found a paper about this : Dependency Graphs for Interactive Theorem Provers (2000) and wonder is there any realization of this idea?

Thanks in advance.
--
Best regards,
Hai WAN

[Coq-Club] The dependency graphs of Coq theorems, Hai WAN
- Re: [Coq-Club] The dependency graphs of Coq theorems, Yves Bertot