diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 22:04:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:52:04 +0200 |
| commit | e11068aa90f6e7fc728d4583998cd99cfa850211 (patch) | |
| tree | 98998fecef98931fea26e5de7d2156c4a6711d42 /plugins/syntax/string_syntax.ml | |
| parent | f19d24a462d50c701a3882de2c16180bb739e622 (diff) | |
[pretyper] Remove imperative passing of evar_map.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions