diff options
| author | Pierre-Marie Pédrot | 2019-03-31 04:09:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-31 04:09:02 +0200 |
| commit | daa9cdd3294d8431e22f2f4b006b0e604230c50f (patch) | |
| tree | cc5a1e64fc8522db872ae1edb16fce5b0c5f2208 /kernel/declareops.ml | |
| parent | 52feb4769d59f0cb843b32d606357194e60d4fc4 (diff) | |
| parent | 6a23ae529bb16b32de7202108ded603d659fa076 (diff) | |
Merge PR #9800: Less conv_tab allocations when pushing relevances, esp skip_pattern
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions