- 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 =
- NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b
- in
- { status with pstatus = n,h,metasenv,subst,o }
+ let status, (_,a) = relocate status ctx a in
+ let status, (_,b) = relocate status ctx b in
+ let n,h,metasenv,subst,o = status#obj in
+ let metasenv, subst = NCicUnification.unify status metasenv subst ctx a b in
+ status#set_obj (n,h,metasenv,subst,o)
+;;
+let unify a b c d = wrap (unify a b c) d;;
+
+let fix_sorts (ctx,t) =
+ let f () =
+ let t = NCicUnification.fix_sorts t in
+ ctx,t
+ in
+ wrap f ()