Cic.metasenv -> (* metasenv *)
Cic.conjecture -> (* sequent *)
Gdome.document * (* Math ML *)
Cic.metasenv -> (* metasenv *)
Cic.conjecture -> (* sequent *)
Gdome.document * (* Math ML *)
(Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
(Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *)
(Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
(Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *)
Gdome.document * (* Math ML *)
(Cic.annobj * (* annobj *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
Gdome.document * (* Math ML *)
(Cic.annobj * (* annobj *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)