+let refinement_toolkit = {
+ RefinementTool.type_of_aux' =
+ (fun ?localization_tbl e c t u ->
+ let saved = !CicRefine.insert_coercions in
+ CicRefine.insert_coercions:= false;
+ let rc =
+ try
+ let t, ty, metasenv, ugraph =
+ CicRefine.type_of_aux' ?localization_tbl e c t u in
+ RefinementTool.Success (t, ty, metasenv, ugraph)
+ with
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s -> RefinementTool.Exception s
+ in
+ CicRefine.insert_coercions := saved;
+ rc);
+ RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+ RefinementTool.apply_subst = CicMetaSubst.apply_subst;
+ RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
+ RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+