diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ef78a953ac..09cf4b0498 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -205,7 +205,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = if cl.cl_strict then Evd.evars_of_term concl else Evar.Set.empty - with _ -> Evar.Set.empty + with e when Errors.noncritical e -> Evar.Set.empty in let hintl = List.map_append @@ -397,7 +397,7 @@ let is_unique env concl = try let (cl,u), args = dest_class_app env concl in cl.cl_unique - with _ -> false + with e when Errors.noncritical e -> false let needs_backtrack env evd oev concl = if Option.is_empty oev || is_Prop env evd concl then |