(* retrieves the list of term that hopefully unify *)
val get_candidates: universe -> Cic.term -> Cic.term list
(* retrieves the list of term that hopefully unify *)
val get_candidates: universe -> Cic.term -> Cic.term list
(* collapse non-indexable terms, not removing coercions *)
val key: Cic.term -> Cic.term
(* collapse non-indexable terms, not removing coercions *)
val key: Cic.term -> Cic.term
(* indexes the term and its unfolded both without coercions *)
val index_term_and_unfolded_term:
universe -> Cic.context -> Cic.term -> Cic.term -> universe
(* indexes the term and its unfolded both without coercions *)
val index_term_and_unfolded_term:
universe -> Cic.context -> Cic.term -> Cic.term -> universe