+ let rec sortify metasenv subst = function
+ | NCic.Implicit (`Typeof _)
+ | NCic.Sort _ as t -> metasenv, subst, t, 0
+ | NCic.Meta (i,_) as t ->
+ let tags, context, ty = NCicUtils.lookup_meta i metasenv in
+ if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
+ else
+ let ty = NCicReduction.whd ~subst context ty in
+ let metasenv, subst, ty, _ = sortify metasenv subst ty in
+ let metasenv, j, m, _ =
+ NCicMetaSubst.mk_meta metasenv [] (`WithType ty)
+ in
+ pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
+ let metasenv,subst = unify test_eq_only metasenv subst context t m in
+ let j = if swap then i else j in
+ let tags, context, ty = NCicUtils.lookup_meta j metasenv in
+ let tags = `IsSort :: tags in
+ let metasenv = List.filter (fun x,_ -> x <> j) metasenv in
+ let metasenv = (j,(tags,context,ty)) ::metasenv in
+ metasenv, subst, m, j
+ | t ->
+ if could_reduce t then raise (Uncertain(lazy "not a sort"))
+ else raise (UnificationFailure(lazy "not a sort"))
+ in
+ let metasenv, subst, _, n =
+ if has_tag ((=) `IsSort) tags then
+ let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
+ in m,s,x,n
+ else if is_sort metasenv subst context t then
+ sortify metasenv subst (NCic.Meta (n,lc))
+ else
+ metasenv, subst, NCic.Rel ~-1,n
+ in
+ let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
+ (* instantiation *)
+
+ (* sortification:
+ - Meta sort === t -> check t is sort or sortify
+ - add tag `IsSort and set cc=[] to n and its pile
+ - se gli ancestor non sono sorte o meta... bum...
+ - cambiare in-place menv
+ - geneare meta fresh sorta e dall'alto al basso
+ - Meta _ === Meta sort -> sortify n (i.e. add `IsSort)
+ *)
+ pp (lazy(string_of_int n ^ " := 111 = "^
+ NCicPp.ppterm ~metasenv ~subst ~context t));