+ | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type)
+ | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
+ | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+ | _ -> assert false
+;;
+
+let force_to_sort metasenv subst context t =
+ match NCicReduction.whd ~subst context t with
+ | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t ->
+ metasenv, subst, t
+ | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) ->
+ metasenv, subst, C.Meta(i,(0,C.Irl 0))
+ | C.Meta (i,(_,lc)) ->
+ let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
+ let metasenv, subst, newmeta =
+ if len > 0 then
+ NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
+ else metasenv, subst, i
+ in
+ metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
+ | C.Sort _ as t -> metasenv, subst, t