diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-14 22:12:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-14 23:33:38 +0200 |
| commit | 7c047370dc9032e3ded3365a45de5b92e7c9033f (patch) | |
| tree | 5da99ed476d2c71a15f4ca2fe09e904411e06a66 /tactics/tacticals.ml | |
| parent | a40451fbd096703d9a06795c9294d11dfd7a74dd (diff) | |
Fix bug #5139: Anomalies should not be caught by || / try.
There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d..66da9ee18 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -322,7 +322,7 @@ module New = struct try Refiner.catch_failerror e; tclUNIT () - with e -> tclZERO e + with e when CErrors.noncritical e -> tclZERO e (* spiwack: I chose to give the Ltac + the same semantics as [Proofview.tclOR], however, for consistency with the or-else |