+prerr_endline ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv
+ instance' ty ugraph
+ in
+prerr_endline ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
+ candidate_oty,ugraph,metasenv,subst
+(* CSC: XXX