- | _ -> [] in
- try
- let rec check_stack f l1 l2 r a =
- match l1,l2,r with
- | x1::tl1, x2::tl2, r::tr ->
- check_stack f tl1 tl2 tr (f x1 x2 r a)
- | x1::tl1, x2::tl2, [] ->
- check_stack f tl1 tl2 tr (f x1 x2 true a)
- | [], [], _ -> a
- | _ -> raise (Invalid_argument "check_stack")
- in
- check_stack
- (fun t1 t2 b (metasenv,subst) ->
- try
- let t1 = RS.from_stack t1 in
- let t2 = RS.from_stack t2 in
- unif_machines metasenv subst (small_delta_step t1 t2)
- with UnificationFailure _ | Uncertain _ when not b ->
- metasenv, subst)
- s1 s2 relevance (metasenv,subst)
- with Invalid_argument _ ->
- raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
- ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
- ~metasenv ~subst ~context (R.unwind m2))))
- with UnificationFailure _ | Uncertain _ when delta > 0 ->
- let delta = delta - 1 in
- let red = R.reduce ~delta ~subst context in
- unif_machines metasenv subst (red m1,red m2,delta)
- in
- let height_of = function
- | NCic.Const (Ref.Ref (_,Ref.Def h))
- | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
- | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
- | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
- | NCic.Meta _ -> max_int
- | _ -> 0
- in
- let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
- let h1 = height_of t1 in
- let h2 = height_of t2 in
- let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
- R.reduce ~delta ~subst context m1,
- R.reduce ~delta ~subst context m2,
- delta
+ | _ -> [] *) in
+ let unif_from_stack t1 t2 b metasenv subst =
+ try
+ let t1 = NCicReduction.from_stack t1 in
+ let t2 = NCicReduction.from_stack t2 in
+ unif_machines metasenv subst (put_in_whd t1 t2)
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ let rec check_stack l1 l2 r (metasenv, subst) =
+ match l1,l2,r with
+ | x1::tl1, x2::tl2, r::tr ->
+ check_stack tl1 tl2 tr
+ (unif_from_stack x1 x2 r metasenv subst)
+ | x1::tl1, x2::tl2, [] ->
+ check_stack tl1 tl2 []
+ (unif_from_stack x1 x2 true metasenv subst)
+ | l1, l2, _ ->
+ fo_unif test_eq_only metasenv subst
+ (NCicReduction.unwind (k1,e1,t1,List.rev l1))
+ (NCicReduction.unwind (k2,e2,t2,List.rev l2))
+ in
+ try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+ with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+ unif_machines metasenv subst (small_delta_step m1 m2)
+ (*D*) in outside(); rc with exn -> outside (); raise exn