diff options
| author | Emilio Jesus Gallego Arias | 2019-10-28 16:16:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-29 17:02:36 +0100 |
| commit | 6986bb7e16523c62776628558a9ec8e7c6b028a7 (patch) | |
| tree | 876cd032f13f9b32890f539761fd75dc4a4296e9 /kernel/nativelambda.ml | |
| parent | e9dddcb2b5297f2e601a2e2d65a131ee5fde19e4 (diff) | |
[abstract] Remove un-unused reference to `evar_map`
We use an `evar_map ref` even tho the modification the `evar_map` is
ignored.
I'm not sure if this is a bug or not, so I am making thus preserving
the behavior but making the what is going with the `evar_map` more
explicit.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions