- [] -> []
- | None::tl -> None::(erase (i+1) tl)
- | he::tl ->
- let i' = (List.nth l (i-1)) in
- if i' <= k
- then he::(erase (i+1) tl) (* local variable *)
- else
- let acc =
- (try List.nth canonical_context (i'-k-1)
- with Failure _ -> None) in
- if acc = None
- then None::(erase (i+1) tl)
- else he::(erase (i+1) tl) in
+ [] -> []
+ | None::tl -> None::(erase (i+1) tl)
+ | he::tl ->
+ let i' = (List.nth l (i-1)) in
+ if i' <= k
+ then he::(erase (i+1) tl) (* local variable *)
+ else
+ let acc =
+ (try List.nth canonical_context (i'-k-1)
+ with Failure _ -> None) in
+ if acc = None
+ then None::(erase (i+1) tl)
+ else he::(erase (i+1) tl) in