diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-05 17:13:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-05 17:26:51 +0200 |
| commit | 6cf0e98fcaf597ef175312bee24042db2677978f (patch) | |
| tree | cf9281f892848ccba8284e91685a6e1226b661e9 /interp | |
| parent | ebb1048bd242e461ed4ecde16583592a18d62c11 (diff) | |
Fast path in push_rel_context_to_named_context.
Essentially, we do not reconstruct the named_context_val when the rel_context
is empty.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions