Useless old code for ad-hoc management of out-scope removed.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c9ebbb93e3c269782f907802956c2c89b8d98b82..1a667770b4ec47b762c8c3d27e090310d2f16f4b 100644 (file)
--- 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 =