diff options
| author | Frédéric Besson | 2016-08-31 19:12:15 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2016-08-31 19:12:15 +0200 |
| commit | 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f (patch) | |
| tree | 38851b455ef429d861f46ef7fc4639233254bd1a /kernel/nativecode.ml | |
| parent | 985e83e60b6665d17b81830aea4fce3384fe2b5a (diff) | |
Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions