+ | CicUnification.Uncertain _ as e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
+ (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+ (candidate, eq_URI))
+ in
+ let c, other, eq_URI =
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
+ in
+ if o <> U.Incomparable then
+ try
+ let res = do_match c eq_URI in
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl)
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ else
+ try
+ let res = do_match c eq_URI in
+ match res with
+ | _, s, _, _, _ ->
+ let c' = apply_subst s c
+ and other' = apply_subst s other in
+ let order = cmp c' other' in
+ let names = U.names_of_context context in
+ if order <> U.Lt && order <> U.Le then
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl)
+ else
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->