| `WithType ty ->
let len = List.length context in
let menv_entry = (n, (name, context, ty)) in
| `WithType ty ->
let len = List.length context in
let menv_entry = (n, (name, context, ty)) in
- menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty
+ menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
mk_meta (tyof name) (newmeta ()) metasenv context `Sort in
mk_meta name n metasenv context (`WithType ty)
| `Term ->
mk_meta (tyof name) (newmeta ()) metasenv context `Sort in
mk_meta name n metasenv context (`WithType ty)
| `Term ->
mk_meta (tyof name) (newmeta ()) metasenv context `Type in
mk_meta name n metasenv context (`WithType ty)
in
mk_meta (tyof name) (newmeta ()) metasenv context `Type in
mk_meta name n metasenv context (`WithType ty)
in
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
mk_meta ~name:name metasenv context (`WithType s) in
let t, metasenv1, args, pno =
aux metasenv1 (NCicSubstitution.subst arg t)
mk_meta ~name:name metasenv context (`WithType s) in
let t, metasenv1, args, pno =
aux metasenv1 (NCicSubstitution.subst arg t)