The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello --

Is there a way to find all the globals that occur in a term? I tried something like this:

repeat match goal with

         | [ |- context [ ?G ] ] =>

           let x := eval cbv delta [ G ] in G in

           idtac "found" G

       end.

But this does not find globals under binders.

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/