(* *)
(******************************************************************************)
+val type_of_aux' : (Cic.context -> Cic.term -> Cic.term) ref
+val lift : (int -> Cic.term -> Cic.term) ref
+
val deannotate_term : Cic.annterm -> Cic.term
+val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv
val deannotate_obj : Cic.annobj -> Cic.obj