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};;
module CicHash :