ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
(* t1, t2 must be well-typed *)
let are_convertible ?(subst=[]) ?(metasenv=[]) =
(* t1, t2 must be well-typed *)
let are_convertible ?(subst=[]) ?(metasenv=[]) =
let rec aux test_equality_only context t1 t2 =
let aux2 test_equality_only t1 t2 =
(* this trivial euristic cuts down the total time of about five times ;-) *)
(* this because most of the time t1 and t2 are "sintactically" the same *)
let rec aux test_equality_only context t1 t2 =
let aux2 test_equality_only t1 t2 =
(* this trivial euristic cuts down the total time of about five times ;-) *)
(* this because most of the time t1 and t2 are "sintactically" the same *)