| Some bo -> aux (ctx,bo))
| (name, src)::ctx, (NCic.Appl args as bo)
when HExtlib.list_last args = NCic.Rel 1 ->
- let args, _ = HExtlib.split_nth (List.length args - 1) args in
+ let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in
(match delift_if_not_occur (NCic.Appl args) with
| None -> aux (ctx,NCic.Lambda(name,src, bo))
| Some bo -> aux (ctx,bo))
unify hdb test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
- | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when
- not (NCicMetaSubst.flexible subst args) &&
- is_locked n subst &&
- not (List.mem_assoc i subst)
- ->
- (* we verify that none of the args is a Meta,
- since beta expanding w.r.t a metavariable makes no sense *)
- let metasenv, lambda_Mj =
- lambda_intros metasenv subst context t1 args
- in
- let metasenv, subst =
- unify hdb test_eq_only metasenv subst context
- (C.Meta (i,l)) lambda_Mj
- in
+ | _, NCic.Meta (n, _) when is_locked n subst ->
+ (let (metasenv, subst), i =
+ match NCicReduction.whd ~subst context t1 with
+ | NCic.Appl (NCic.Meta (i,l)::args) when
+ not (NCicMetaSubst.flexible subst args)
+ ->
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args
+ in
+ unify hdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj,
+ i
+ | NCic.Meta (i,_) -> (metasenv, subst), i
+ | _ -> assert false
+ in
let t1 = NCicReduction.whd ~subst context t1 in
let j, lj =
- match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+ match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
in
let metasenv, subst =
instantiate hdb test_eq_only metasenv subst context j lj t2 true
let term = eta_reduce subst term in
let subst = List.filter (fun (j,_) -> j <> i) subst in
metasenv, ((i, (name, ctx, term, ty)) :: subst)
- with Not_found -> assert false)
+ with Not_found -> assert false))
| C.Meta (n,lc), t ->
(try
let relevance = NCicEnvironment.get_relevance r1 in
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
- let _,relevance = HExtlib.split_nth lno relevance in
+ let relevance =
+ try snd (HExtlib.split_nth "NU 2" lno relevance)
+ with Failure _ -> []
+ in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
(*D*) in outside(); rc with exn -> outside (); raise exn
;;
-let unify hdb =
+let unify hdb ?(test_eq_only=false) =
indent := "";
- unify hdb false;;
-
-
+ unify hdb test_eq_only;;