(("_",C.Decl ty_arg) :: context) `Type
in
let flex_prod = C.Prod ("_", ty_arg, meta) in
+ (* next line grants that ty_args is a type *)
+ let metasenv,subst, flex_prod, _ =
+ typeof ~look_for_coercion ~localise metasenv subst
+ context flex_prod None in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
^ "\nOF: " ^