- let restrict metasenv subst = function
- | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t ->
- metasenv, subst, t
- | C.Meta (i,(_,lc)) as t ->
- let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
- let metasenv, subst, _ =
- NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len)
- in
- metasenv, subst, t
- | t -> metasenv, subst, t
- in
- let t1 = NCicReduction.whd ~subst context t1 in
- let t2 = NCicReduction.whd ~subst ((name,C.Decl s)::context) t2 in
- let metasenv, subst, t1 = restrict metasenv subst t1 in
- let metasenv, subst, t2 = restrict metasenv subst t2 in
+ let metasenv, subst, t1 = force_to_sort metasenv subst context t1 in
+ let metasenv, subst, t2 =
+ force_to_sort metasenv subst ((name,C.Decl s)::context) t2 in
+ prerr_endline ("S1:"^NCicPp.ppterm ~metasenv ~subst ~context t1);
+ prerr_endline ("S2:"^NCicPp.ppterm ~metasenv ~subst ~context:((name,C.Decl s)::context) t2);