diff options
| author | Maxime Dénès | 2014-07-31 01:06:04 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-31 01:08:33 -0400 |
| commit | 2b8c1b9dc688e3e6bf5c6ed77f1ad7864e1f281c (patch) | |
| tree | 5f4b3e54d01de3e824d8610c083a8a85f71b4eb7 /kernel/cbytecodes.ml | |
| parent | 8547814ac99a8f22875ecb3a3f42958e9a82f208 (diff) | |
Optimize check of new subterm relation on match.
If the return predicate is not dependent, we avoid dynamically regenerating the
regular tree of the corresponding inductive type. This includes the commutative
cut rule. Should solve some performance issues observed in Compcert and Paco at
Qed time.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions