+ NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1))))
+ | NCic.Irl len, NCic.Irl len1
+ when shift1 < shift || len1 + shift1 > len + shift ->
+ (* C. Hoare. Premature optimization is the root of all evil*)
+ let stop = shift + len in
+ let stop1 = shift1 + len1 in
+ let low_gap = max 0 (shift - shift1) in
+ let high_gap = max 0 (stop1 - stop) in
+ let restrictions =
+ HExtlib.list_seq (k+1-shift1) (low_gap + 1) @
+ HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
+ in
+ let metasenv, subst, newmeta =
+ restrict metasenv subst i restrictions
+ in
+(*
+ prerr_endline ("RESTRICTIONS FOR: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:[]
+ (NCic.Meta (i,l1))^" that was part of a term unified with "
+ ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta
+ (n,l)) ^ " ====> " ^ String.concat "," (List.map
+ string_of_int restrictions) ^ "\nMENV:\n" ^
+ NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^
+ NCicPp.ppsubst subst ~metasenv);
+*)
+ let newlc_len =
+ len1 - low_gap - high_gap + max 0 (k - shift1) in
+ assert (if shift1 > k then
+ shift1 + low_gap - shift = 0 else true);
+ let meta =
+ NCic.Meta(newmeta,(shift1 + low_gap - shift,
+ NCic.Irl newlc_len))
+ in
+ let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
+ assert (List.length cctx = newlc_len);
+ (metasenv, subst), meta
+