Cic.metasenv -> (* metasenv *)
Cic.conjecture -> (* sequent *)
Gdome.document * (* Math ML *)
+ Cic.conjecture * (* unshared sequent *)
(Cic.annconjecture * (* annsequent *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
(Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)