The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Hyung,

I think that the command you are looking for is SearchAbout, especially
the 4th (and following) variants described in the reference manual [1].
These are the most powerful variants of SearchAbout.

Regarding your second question, Anne Pacalet wrote tools [2] to build
dependency graphs of Coq objects (axioms / definitions / lemmas / etc.).
You will need to compile your own  [coqtop].

The dependencies between modules are well determined by coqdep
but I guess that being able to dump the DAG would however require
writing a patch.
If you have problems to compile your project by hand, you should
consider using coq_makefile which will do all the hard work for you
(like invoking coqdep and use the result to compile in a meaningful order).

Cheers,
--
guillaume

[1] 
http://coq.inria.fr/refman/Reference-Manual009.html#@command115
[2] http://www-sop.inria.fr/members/Anne.Pacalet/tools.php#DpdGraph


2011/8/13 ê¹€í˜•ì„  
<hskiowa AT kaist.ac.kr>
>
> Hello.
>
>
>
> This is the first time I email to coq-club.
>
>
>
> I am an undergradate student in Korea, and I have been recently using coq 
> program for a few months.
>
>
>
> Here are two questions:
>
>
>
> 1. Search commands do not search beyond definitions. I mean it doesn't go 
> through delta reductions.
>
>
>
> What should I do if I want to search for definitions related to a keyword?
>
>
>
> 2. There are many coq script files in a folder. They inherit among 
> themselves using commands such as  "Require Import/Export blabla."
>
>
>
> Is there a program to view a "genealogy tree" of the files? I think it 
> would come in handy when compiling or adjusting files.
>
>
>
> Is there a program to view a "genealogy tree" for definitions/theorems? 
> This will be very useful, for instance, in figuring out how powerful an 
> axiom/a theorem is.
>
>
>
>
>
> Hyung Sun Kim
>
> Department of Mathematical Sciences in KAIST