- (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
- in
- let c, other, eq_URI =
- if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
- else right, left, HL.Logic.eq_ind_r_URI
- in
- if o <> U.Incomparable then
- try
- let res = do_match c other eq_URI in
- res::(find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl)
- with e ->
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
- else
- try
- let res = do_match c other eq_URI in
- match res with
- | _, s, _, _, _ ->
- let c' = (* M. *)apply_subst s c
- and other' = (* M. *)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 tl)
- else
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
- with e ->
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
+ let c, other, eq_URI =
+ if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
+ else right, left, HL.Logic.eq_ind_r_URI
+ in
+ if o <> U.Incomparable then
+ try
+ let res = do_match c other eq_URI in
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl)
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+ else
+ try
+ let res = do_match c other eq_URI in
+ match res with
+ | _, s, _, _, _ ->
+ let c' = (* M. *)apply_subst s c
+ and other' = (* M. *)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 tl)
+ else
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl