The patch was used to nullify items in the local context when they where
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
let delift n subst context metasenv l t =
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
let delift n subst context metasenv l t =
- let l =
- let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
- List.map2 (fun ct lt ->
- match (ct, lt) with
- | None, _ -> None
- | Some _, _ -> lt)
- canonical_context l
- in
let module S = CicSubstitution in
let to_be_restricted = ref [] in
let rec deliftaux k =
let module S = CicSubstitution in
let to_be_restricted = ref [] in
let rec deliftaux k =