- Cic.conjecture -> (* conjecture *)
- Cic.annconjecture * (* annotated conjecture *)
- (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
- (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
- (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
- (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)
-
+ Cic.conjecture -> (* sequent *)
+ Cic.conjecture * (* unshared sequent *)
+ (Cic.annconjecture * (* annotated sequent *)
+ (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
+ (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t) (* ids_to_hypotheses *)
+
+val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj