diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index b7f6addc..e4b3bdb1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -497,7 +497,7 @@ let wrap_inv_error id = function (* The most general inversion tactic *) let inversion inv_kind status names id gls = try (raw_inversion inv_kind id status names) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e (* Specializing it... *) @@ -540,7 +540,7 @@ let invIn k names ids id gls = inversion (false,k) NoDep names id; intros_replace_ids]) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e let invIn_gen k names idl = try_intros_until (invIn k names idl) |