The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> From the ml code inside the "arewrite" tactic, I need to traverse the
> environment and retrieve the "fact" and "ac_plus" declarations.  It would 
> also
> be useful to traverse the declarations in any modules that are imported.  
> How
> can I do this?

I suspect that your question was finally more about looking up a
declaration in the environment and that Talia answered. If it is
really about traversing the environment, as e.g. "Search" or "Print
All" would do, I wrote a little general-purpose answer on the wiki,
recently moved to GitHub 
(https://github.com/coq/coq/wiki/Development-questions).

Best,

Hugo Herbelin

On Fri, Nov 17, 2017 at 02:21:23PM +0000, Kenneth Roe wrote:
> One of the requirements for my "arewrite" tactic is the ability to walk 
> through
> and collect all available definitions from the environment.  Consider a Coq
> source file with the following:
> 
> 
> Require Import AdvancedRewrite.advancedRewrite.
> 
> 
> Fixpoint fact (x : nat) := match x with        
> 
> 0 => 1
> 
> S n => fact n
> 
> end.
> 
> 
> Theorem ac_plus: AC plus.
> 
> 
> Theorem test1: fact 4 = 24.
> 
> Proof.
> 
>     arewrite.
> 
> Abort.
> 
> 
> From the ml code inside the "arewrite" tactic, I need to traverse the
> environment and retrieve the "fact" and "ac_plus" declarations.  It would 
> also
> be useful to traverse the declarations in any modules that are imported.  
> How
> can I do this?
> 
> 
>                        - Ken
> 
>