- match l with
- | shift, NCic.Irl len ->
- let restrictions =
- List.filter
- (fun i -> i > shift && i <= shift + len) restrictions in
- ms, restrictions, mk_restricted_irl shift len restrictions
- | shift, NCic.Ctx l ->
- let ms, _, restrictions_for_n, l =
- List.fold_right
- (fun t (ms, i, restrictions_for_n, l) ->
- try
- let ms, t = aux (k-shift) ms t in
- ms, i-1, restrictions_for_n, t::l
- with Occur ->
- ms, i-1, i::restrictions_for_n, l)
- l (ms, List.length l, [], [])
- in
- ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
+ let l = NCicUtils.expand_local_context lc in
+ let ms, _, restrictions_for_n, l =
+ List.fold_right
+ (fun t (ms, i, restrictions_for_n, l) ->
+ try
+ let ms, t = aux (k-shift) ms t in
+ ms, i-1, restrictions_for_n, t::l
+ with Occur ->
+ ms, i-1, i::restrictions_for_n, l)
+ l (ms, List.length l, [], [])
+ in
+ ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)