diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c352a6ac1f..1c24578a1c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1944,7 +1944,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = try (* First try finding a subterm w/o conversion on open terms *) let flags = set_no_delta_open_flags flags in w_unify_to_subterm env evd ~flags t' - with e -> + with e when CErrors.noncritical e -> (* If this fails, try with full conversion *) w_unify_to_subterm env evd ~flags t' else w_unify_to_subterm env evd ~flags t' |