+let purge_restricted restrictions more_restrictions l =
+ if more_restrictions = [] then l
+ else
+ begin
+ pp (lazy ("TO BE RESTRICTED: " ^
+ (String.concat "," (List.map string_of_int restrictions))));
+ pp (lazy ("MORE RESTRICTIONS: " ^
+ (String.concat "," (List.map string_of_int more_restrictions))));
+ let shift,lc = l in
+ let lc = NCicUtils.expand_local_context lc in
+ let rec aux n lc =
+ match lc with
+ [] -> []
+ | _ when List.mem n restrictions -> aux (n+1) lc
+ | _::tl when List.mem n more_restrictions -> aux (n+1) tl
+ | he::tl -> he::aux (n+1) tl
+ in
+ pack_lc (shift, NCic.Ctx (aux 1 lc))
+ end
+;;
+