Better navigation commands for modular development

[GoogleCodeExporter]

Well, this is something we probably want to ignore as we are getting closer
to the high-level language. But anyway...

I'm trying to work with a module (because I've not-so-nice shared
parameters), so I do:

> module Bla;
> lambda Param1 : Set;

Then, I solve a programming problem:

> let foo (...) : Set;
> ...

When I'm done, I'm somewhere randomly deep in my development. Then, I would
like to make a new definition, potentially using "foo".

I know no other way but doing:

> root;
> jump Bla.foo; -- (or any definition in Bla)
> out;

So, am I missing something? Or we need a small tactics that gets us
directly to the "top" of a module by its name?

Original issue reported on code.google.com by pedag...@gmail.com on 6 Jun 2010 at 1:05

[GoogleCodeExporter]

I think we want a tactic to jump to the bottom of the development that contains 
the programming problem you are working on. This should probably be called 
automatically when you solve the last goal in a problem. Does that sound 
reasonable?

Original comment by adamgundry on 10 Jun 2010 at 9:05

• Changed state: Accepted