exception ListTooShort
exception RelToHiddenHypothesis
-val syntactic_equality_add_time: float ref
-val type_of_aux'_add_time: float ref
-val number_new_type_of_aux'_double_work: int ref
-val number_new_type_of_aux': int ref
-val number_new_type_of_aux'_prop: int ref
-
type types = {synthesized : Cic.term ; expected : Cic.term option};;
+val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
+
val double_type_of :
Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
types Cic.CicHash.t