;;
let unify a b c d = wrap (unify a b c) d;;
+let fix_sorts (name,ctx,t) =
+ let f () =
+ let t = NCicUnification.fix_sorts t in
+ name,ctx,t
+ in
+ wrap f ()
+;;
+
let refine status ctx term expty =
let status, (nt,_,term) = relocate status ctx term in
let status, ne, expty =