- prerr_endline
- (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
- proofterm);
- let _metasenv, _subst, _proofterm, _prooftype =
- NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
+ prerr_endline (NCicPp.ppterm ~metasenv:C.metasenv
+ ~subst:C.subst ~context:C.context proofterm);
+ let metasenv, subst, proofterm, _prooftype =
+ NCicRefiner.typeof
+ (rdb#set_coerc_db NCicCoercion.empty_db)
+ C.metasenv C.subst C.context proofterm None