fo_unif_subst subst context metasenv newhety expty ugraph
in
let b, ugraph =
- CicReduction.are_convertible ~subst context infty expty ugraph
+ CicReduction.are_convertible
+ ~subst ~metasenv context infty expty ugraph
in
if b then
Some ((t,infty), subst, metasenv, ugraph)