--- /dev/null
+exception Impossible of int
+exception NotWellTyped of string
+exception WrongUriToConstant of string
+exception WrongUriToVariable of string
+exception WrongUriToMutualInductiveDefinitions of string
+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 double_type_of :
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
+ types Cic.CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool