delift_rels_from subst metasenv 1 n t
*)
+let mk_meta ?name metasenv context ty =
+ let n = newmeta () in
+ let len = List.length context in
+ let menv_entry = (n, (name, context, ty)) in
+ menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len))
+;;
+
+let saturate ?(delta=0) metasenv context ty goal_arity =
+ assert (goal_arity >= 0);
+ let rec aux metasenv = function
+ | NCic.Prod (name,s,t) ->
+ let metasenv1, arg = mk_meta ~name:name metasenv context s in
+ let t, metasenv1, args, pno =
+ aux metasenv1 (NCicSubstitution.subst arg t)
+ in
+ if pno + 1 = goal_arity then
+ ty, metasenv, [], goal_arity+1
+ else
+ t, metasenv1, arg::args, pno+1
+ | ty ->
+ match NCicReduction.whd context ty ~delta with
+ | NCic.Prod _ as ty -> aux metasenv ty
+ | ty -> ty, metasenv, [], 0
+ in
+ let res, newmetasenv, arguments, _ = aux metasenv ty in
+ res, newmetasenv, arguments
+;;