diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-25 14:04:49 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-29 22:16:07 +0200 |
| commit | 38da14404781843a6143fc4af9d503e05d8d7dd6 (patch) | |
| tree | ca11ea317485d4f37ae9dd08608ea973d5eeefe2 /tactics | |
| parent | 671e556453c1eee335cf788ebc72675f5a7483d8 (diff) | |
class_tactics: remove catch-all, use Errors.noncritical
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 ef78a953a..09cf4b049 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 |