- match ty with
- | `Typeless ->
- let n = newmeta () in
- let ty = NCic.Implicit (`Typeof n) in
- let menv_entry = (n, (name, context, ty)) in
- menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty
- | `Type
- | `Term ->
- let context_for_ty = if ty = `Type then [] else context in
- let n = newmeta () in
- let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in
- let m = newmeta () in
- let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in
- let menv_entry = (m, (name, context, ty)) in
- menv_entry :: ty_menv_entry :: metasenv,
- NCic.Meta (m, (0,NCic.Irl (List.length context))), ty
+ let tyof = function Some s -> Some ("typeof_"^s) | None -> None in
+ let rec mk_meta name n metasenv context = function