From e20e61bf6ec3f40451fd06059ac9293d9c45538c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 Oct 2009 10:21:38 +0000 Subject: [PATCH] Useless old code for ad-hoc management of out-scope removed. --- .../components/ng_refiner/nCicUnification.ml | 25 ------------------- 1 file changed, 25 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index c9ebbb93e..1a667770b 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -385,31 +385,6 @@ 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 context metasenv subst) -(* - | kind, ty, NCic.Meta(m,lcm), _ when List.mem_assoc m subst -> - let at,ccm,bo,tym = NCicUtils.lookup_subst m subst in - if NCicMetaSubst.is_out_scope_tag at then - begin - (* Case meta vs out-scope *) - pp(lazy("4.1")); - let ty_t, ccm, kindm = - NCicSubstitution.subst_meta lcm tym, ccm, - NCicUntrusted.kind_of_meta at in - let lty = NCicSubstitution.subst_meta lc ty in - pp (lazy ("On the types: " ^ - ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ - ppterm ~metasenv ~subst ~context ty_t)); - let metasenv, subst = - unify rdb false metasenv subst context ty_t lty in - (*CSC: here I should call kindfy, but it fails since the second - meta in in the susbt, not the metasenv! *) - (* let metasenv,subst,t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in *) - delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst - end - else - let bo = NCicSubstitution.subst_meta lcm bo in - instantiate rdb test_eq_only metasenv subst context n lc bo swap -*) (*D*) in outside None; rc with exn -> outside (Some exn); raise exn and unify rdb test_eq_only metasenv subst context t1 t2 = -- 2.39.2