let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
if o <> U.Incomparable then
try
do_match c other eq_URI
- with e ->
+ with Inference.MatchingFailure ->
find_matches metasenv context ugraph lift_amount term tl
else
- let res = try do_match c other eq_URI with e -> None in
+ let res =
+ try do_match c other eq_URI
+ with Inference.MatchingFailure -> None
+ in
match res with
| Some (_, s, _, _, _) ->
let c' = (* M. *)apply_subst s c
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
let res = do_match c other eq_URI in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term tl)
- with e ->
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term tl
else
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
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
;;
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
samesubst subst subst'
- with e ->
+ with Inference.MatchingFailure ->
false
in
let r = List.exists (ok right) leftr in