X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=035e65ac7b83089cd086b803045c8b24f165ed51;hb=5366f90df289f2ab2bd97c68643198f54ad2d2ac;hp=52a45bbd49dd83a2267997f0b9532cf9313753d2;hpb=d44567ba4b1a658974ee353e67c05d114c264f7f;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 52a45bbd4..035e65ac7 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -152,6 +152,14 @@ let unify status ctx a b =
 ;;
 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 =