diff options
| author | Pierre-Marie Pédrot | 2018-06-28 18:36:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 20:15:18 +0200 |
| commit | 86d08ece4c63e2a42f72ddd3afc51ce04cd1932a (patch) | |
| tree | 314eac7625739d9047b4210e8622695b0007e884 /kernel/nativelib.ml | |
| parent | 7cc70b0df61718a946327d5bfb056b140eeb54ba (diff) | |
Fix an algorithmic issue in the vernac guardedness checker.
Calling the O(n) EConstr.to_constr function at every node is a very bad
idea (tm).
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions