The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

> 1) is there some way of finding out which "Section"'s are currently open?

Yes, with the command Inspect you can see the last introduced objects
in the Coq environment, including opening of sections. The argument to
inpsect is the number of objects you want to see:

======================================================================
Coq < Section A.
Coq < Section B.
Coq < Section B.
Coq < Inspect 5.
 >>>>>>> Import Program
 >>>>>>> Import Prolog
 >>>>>>> Section A
 >>>>>>> Section B
 >>>>>>> Section C
======================================================================

> 2) is there some way of finding out which "Axiom"'s are currently  
> available/being assumed?

Still with the command Inspect you will see axioms, prefixed with
"***"
======================================================================
Coq < Parameter T:Set.
T is assumed

Coq < Inspect 4.
 >>>>>>> Section A
 >>>>>>> Section B
 >>>>>>> Section C
*** [ T : Set ]
======================================================================

But unfortunately, you will not see axioms coming from imported
modules. Example:
======================================================================
Coq < Require List.
Coq < Inspect 5.
...
 >>>>>>> Import List
======================================================================
You just see "Import List" but you do not see the parameter List_Dom
defined in the module List.

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr