match candidate with
| None -> raise (Uncertain "can't solve an higher order unification problem")
| Some candidate ->
- prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
let s,m,u =
fo_unif_subst subst context metasenv
candidate outtype ugraph5