- let metasenv, subst =
- if swap then
- unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
- else
- unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
- in
- (metasenv, subst), NCic.Rel (1 + n)
- with Uncertain _ | UnificationFailure _ ->
- match t' with
- | NCic.Rel m as orig ->
- (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
- (* andrea: in general, beta_expand can create badly typed
- terms. This happens quite seldom in practice, UNLESS we
- iterate on the local context. For this reason, we renounce
- to iterate and just lift *)
- | NCic.Meta (i,(shift,lc)) ->
- (metasenv,subst), NCic.Meta (i,(shift+1,lc))
- | NCic.Prod (name, src, tgt) as orig ->
- let (metasenv, subst), src1 = aux (n,context,true) acc src in
- let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
- let ms, tgt1 = aux k (metasenv, subst) tgt in
- if src == src1 && tgt == tgt1 then ms, orig else
- ms, NCic.Prod (name, src1, tgt1)
- | t ->
- NCicUntrusted.map_term_fold_a
- (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t