* likely to know the exact value of the result e.g. if the rhs is a
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
- CicMkImplicit.mk_implicit metasenv [] in
+ CicMkImplicit.mk_implicit_sort metasenv in
let (subst, metasenv) =
CicUnification.fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2''