diff options
| author | Pierre-Marie Pédrot | 2017-04-11 15:48:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-12 13:59:31 +0200 |
| commit | 71d71554b7b3b0e50f67d5d1c4428c1ec4e6fa44 (patch) | |
| tree | f4952c708dab98506f2d6b44d3123ebba9b42dac /API/grammar_API.ml | |
| parent | f41944730792070d4a3074aa1fe1f8465062b758 (diff) | |
Missing optimization when Kernel Term Sharing is disabled.
We don't have to perfom in-place updates because we actually know that there
is none on the stack. This should speed up UniMath.
Diffstat (limited to 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions