refreshing of inferred type was missing

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index ede2e856afb845b2f7205f6c70550c09f4404047..96cd29606493ce1eac22b671ad6c8a389cd8ee99 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -735,7 +735,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
 
 let sort_of subst metasenv ctx t =
   let ty = NCicTypeChecker.typeof subst metasenv ctx t in
-    NCicTypeChecker.typeof subst metasenv ctx ty
+  let metasenv',ty = NCicUnification.fix_sorts metasenv subst ty in
+   assert (metasenv = metasenv');
+   NCicTypeChecker.typeof subst metasenv ctx ty
 ;;
   
 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
@@ -1227,7 +1229,6 @@ auto_main flags signature (cache:cache) depth status: unit =
     | orig::_ ->
        if depth > 0 && move_to_side depth status
        then 
-         let _ = print (lazy "merged") in
          let status = NTactics.merge_tac status in
            auto_clusters flags signature cache (depth-1) status 
        else