mk_meta name (newmeta ()) metasenv context ty
;;
-let saturate ?(delta=0) metasenv context ty goal_arity =
+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 =
else
t, metasenv1, arg::args, pno+1
| ty ->
- match NCicReduction.whd context ty ~delta with
+ match NCicReduction.whd ~subst context ty ~delta with
| NCic.Prod _ as ty -> aux metasenv ty
| ty -> ty, metasenv, [], 0
in