From 123e66ead6ee8f502bd2fc2baf5482fe78ae6f34 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 24 Nov 2009 16:56:59 +0000 Subject: [PATCH] Bugfix in tipify: a metavariable was set to type without sortifying its type. --- .../components/ng_refiner/nCicUnification.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 466c0ef85..c7b487461 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -241,9 +241,11 @@ let tipify exc metasenv subst context t ty = if is_type attrs then metasenv,subst,true else + let _,cc,ty = NCicUtils.lookup_meta n metasenv in + let metasenv,subst,ty = sortfy exc metasenv subst cc ty in let metasenv = NCicUntrusted.replace_in_metasenv n - (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty) + (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty) metasenv in metasenv,subst,false @@ -253,9 +255,11 @@ let tipify exc metasenv subst context t ty = if is_type attrs then metasenv,subst,true else + let _,cc,_,ty = NCicUtils.lookup_subst n subst in + let metasenv,subst,ty = sortfy exc metasenv subst cc ty in let subst = NCicUntrusted.replace_in_subst n - (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) + (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) subst in optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo)) @@ -354,8 +358,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> assert false) | `IsType | `IsTerm -> - (match ty,t with - NCic.Implicit (`Typeof _), _ -> + (match ty with + NCic.Implicit (`Typeof _) -> let (metasenv, subst), ty_t = try NCicMetaSubst.delift @@ -375,7 +379,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = in delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv subst - | _, _ -> + | _ -> let lty = NCicSubstitution.subst_meta lc ty in pp (lazy ("On the types: " ^ ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ -- 2.39.2