diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-19 14:21:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-19 16:36:16 +0200 |
| commit | 9bc2b3d6d0f7d02843180bca5a4d1f908e8a6141 (patch) | |
| tree | bb59d34f0800f13ed0117d1d83b1b7cfcda8e9a0 /vernac/metasyntax.ml | |
| parent | 7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff) | |
An optimization of tactic constructor.
As was questioned on Stack Overflow and discussed on Gitter, reduction
of the conclusion of the goal was done up to n+1 times for a failing
call to "constructor" on an inductive type of n constructors. We do it
at most once.
Reworking the layout of the code at the same time.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions