CicTypeChecker.type_of_aux' ~subst metasenv context c
CicUniv.empty_ugraph in
let _,metasenv,args,lastmeta =
- TermUtil.saturate_term freshmeta metasenv context ty arity in
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in