let unify status ctx a b =
let status, (_,_,a) = relocate status ctx a in
let status, (_,_,b) = relocate status ctx b in
let n,h,metasenv,subst,o = status.pstatus in
let metasenv, subst =
let unify status ctx a b =
let status, (_,_,a) = relocate status ctx a in
let status, (_,_,b) = relocate status ctx b in
let n,h,metasenv,subst,o = status.pstatus in
let metasenv, subst =