1 exception Impossible of int
2 exception NotWellTyped of string
3 exception WrongUriToConstant of string
4 exception WrongUriToVariable of string
5 exception WrongUriToMutualInductiveDefinitions of string
7 exception RelToHiddenHypothesis
9 val syntactic_equality_add_time: float ref
10 val type_of_aux'_add_time: float ref
11 val number_new_type_of_aux'_double_work: int ref
12 val number_new_type_of_aux': int ref
13 val number_new_type_of_aux'_prop: int ref
15 type types = {synthesized : Cic.term ; expected : Cic.term option};;
17 val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
20 Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
23 (** Auxiliary functions **)
25 (* does_not_occur n te *)
26 (* returns [true] if [Rel n] does not occur in [te] *)
27 val does_not_occur : int -> Cic.term -> bool