From 6c3b2a89bd14bb8a96e56565b725dd635effc2e5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Mar 2010 15:34:34 +0000 Subject: [PATCH] refreshing of inferred type was missing --- helm/software/components/ng_tactics/nnAuto.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index ede2e856a..96cd29606 100644 --- 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 -- 2.39.2