+ let t1 = NCicReduction.whd ~subst context t1 in
+ let j, lj =
+ match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
+ in
+ let metasenv, subst =
+ instantiate rdb test_eq_only metasenv subst context j lj t2 true
+ in
+ (* We need to remove the out_scope_tags to avoid propagation of
+ them that triggers again the ad-hoc case *)
+ let subst =
+ List.map (fun (i,(tag,ctx,bo,ty)) ->
+ let tag =
+ match tag with
+ Some tag when
+ tag = NCicMetaSubst.in_scope_tag
+ || NCicMetaSubst.is_out_scope_tag tag -> None
+ | _ -> tag
+ in
+ i,(tag,ctx,bo,ty)
+ ) subst
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ 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))
+
+ | C.Meta (n,lc), t ->
+ (try
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ unify rdb test_eq_only metasenv subst context term t
+ with NCicUtils.Subst_not_found _->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) false)
+
+ | t, C.Meta (n,lc) ->
+ (try
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ unify rdb test_eq_only metasenv subst context t term
+ with NCicUtils.Subst_not_found _->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) true)
+
+ | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ unify rdb test_eq_only metasenv subst context
+ (mk_appl ~upto:(List.length args) term args) t2
+
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ unify rdb test_eq_only metasenv subst context t1
+ (mk_appl ~upto:(List.length args) term args)
+
+ | NCic.Appl (NCic.Meta (i,_)::_ as l1),
+ NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+ (try
+ List.fold_left2
+ (fun (metasenv, subst) t1 t2 ->
+ unify rdb test_eq_only metasenv subst context t1 t2)
+ (metasenv,subst) l1 l2
+ with Invalid_argument _ ->
+ raise (fail_exc metasenv subst context t1 t2))
+
+ | NCic.Appl (NCic.Meta (i,l)::args), _ ->
+ let metasenv, subst, lambda_Mj =
+ lambda_intros rdb metasenv subst context t1 args
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context t1 t2
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ 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)
+
+ | _, NCic.Appl (NCic.Meta (i,l)::args) ->
+ let metasenv, subst, lambda_Mj =
+ lambda_intros rdb metasenv subst context t2 args
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context
+ lambda_Mj (C.Meta (i,l))
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context t1 t2
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ 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)
+
+ (* processing this case here we avoid a useless small delta step *)
+ | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
+ when Ref.eq r1 r2 ->
+ let relevance = NCicEnvironment.get_relevance r1 in
+ let relevance = match r1 with
+ | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+ let relevance =
+ try snd (HExtlib.split_nth lno relevance)
+ with Failure _ -> []
+ in
+ HExtlib.mk_list false lno @ relevance
+ | _ -> relevance
+ in
+ let metasenv, subst, _ =
+ try
+ List.fold_left2
+ (fun (metasenv, subst, relevance) t1 t2 ->
+ let b, relevance =
+ match relevance with b::tl -> b,tl | _ -> true, [] in
+ let metasenv, subst =
+ try unify rdb test_eq_only metasenv subst context t1 t2
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ metasenv, subst, relevance)
+ (metasenv, subst, relevance) tl1 tl2
+ with Invalid_argument _ ->
+ raise (uncert_exc metasenv subst context t1 t2)
+ in
+ metasenv, subst
+
+ | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+ C.Match (ref2,outtype2,term2,pl2)) ->
+ let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
+ let _,_,ty,_ = List.nth itl tyno in
+ let rec remove_prods ~subst context ty =
+ let ty = NCicReduction.whd ~subst context ty in
+ match ty with
+ | C.Sort _ -> ty
+ | C.Prod (name,so,ta) ->
+ remove_prods ~subst ((name,(C.Decl so))::context) ta
+ | _ -> assert false
+ in
+ let is_prop =
+ match remove_prods ~subst [] ty with
+ | C.Sort C.Prop -> true
+ | _ -> false
+ in
+ if not (Ref.eq ref1 ref2) then
+ raise (uncert_exc metasenv subst context t1 t2)
+ else
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context outtype1 outtype2 in
+ let metasenv, subst =
+ try unify rdb test_eq_only metasenv subst context term1 term2
+ with UnificationFailure _ | Uncertain _ when is_prop ->
+ metasenv, subst