let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
let type_of_aux' metasenv subst context term ugraph =
let foo () =
try
- CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
+ profile.HExtlib.profile
+ (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
with
CicTypeChecker.TypeCheckerFailure msg ->
let msg =
(lower m1 m2) (upper m1 m2) ugraph
in
begin
- let subst,metasenv,ugraph1 =
+ let subst,metasenv,ugraph1 =
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
let tyt,ugraph1 =