let saturate ?(delta=0) metasenv subst context ty goal_arity =
assert (goal_arity >= 0);
let rec aux metasenv = function
- | NCic.Prod (name,s,t) ->
+ | NCic.Prod (name,s,t) as ty ->
let metasenv1, arg,_ =
mk_meta ~name:name metasenv context (`WithType s) in
let t, metasenv1, args, pno =