- let metasenv, subst =
- if swap then
- unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
- else
- unify hdb 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
-
- in
- let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
- let fresh_name = "Hbeta" ^ string_of_int num in
- let (metasenv,subst), t1 =
- aux (0, context, test_eq_only) (metasenv, subst) t in
- let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
- try
- ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
- metasenv, subst, t2
- with NCicTypeChecker.TypeCheckerFailure _ ->
- metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)