"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
(CicPp.ppterm s)))
- with Not_found -> (more @ more_to_be_restricted, metasenv', subst))
+ with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
with Occur ->
raise (MetaSubstFailure (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
(*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 =