Module Vernacstate.Interp
type t={system : System.Interp.t;summary + libstack
lemmas : LemmaStack.t option;proofs of lemmas currently opened
program : Declare.OblState.t NeList.t;program mode table. One per open module/section including the toplevel module.
opaques : Opaques.Summary.t;qed-terminated proofs
}