- | UnificationFailure msg as exn ->
- (try
- unif_machines metasenv subst
- (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
- with
- | UnificationFailure _ -> raise (UnificationFailure msg)
- | Uncertain _ -> raise exn)
- | Uncertain msg as exn ->
-(*
- prerr_endline "PROBLEMA";
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
- let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in
- match
- try_hints metasenv subst
- (NCicReduction.unwind t1) (NCicReduction.unwind t2)
- with
- | Some x -> x
- | None ->
- try
- unif_machines metasenv subst (t1m, t2m)
- with
- | UnificationFailure _ -> raise (UnificationFailure msg)
- | Uncertain _ -> raise exn
- (*D*) in outside true; rc with exn -> outside false; raise exn
+ | UnificationFailure _ as exn -> raise exn
+ | KeepReducing _ | Uncertain _ as exn ->
+ let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+ put_in_whd (0,[],t1,[]) (0,[],t2,[])
+ in
+ (match
+ try_hints metasenv subst
+ (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+ with
+ | Some x -> x
+ | None ->
+ match exn with
+ | KeepReducing msg ->
+ (try
+ unif_machines metasenv subst (tm1,tm2)
+ with
+ | UnificationFailure _ -> raise (UnificationFailure msg)
+ | Uncertain _ -> raise (Uncertain msg)
+ | KeepReducing _ -> assert false)
+ | Uncertain _ -> raise exn
+ | _ -> assert false)
+ (*D*) in outside true; rc with KeepReducing _ -> assert false | exn -> outside false; raise exn