"and those of its inductive type"))))
else
metasenv,subst,item1::context
- ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+ ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
with Invalid_argument "List.fold_left2" -> assert false in
let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
(match