diff options
| author | Hugo Herbelin | 2018-02-26 18:31:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-03-27 19:10:11 +0200 |
| commit | 3e2887bbcba6846ce3a18898fcfebe48632b72b9 (patch) | |
| tree | 4ce4c7b71faaed13e0de28e719bdd7ff192b567b /plugins/syntax/string_notation.ml | |
| parent | 157218226997281ddb674899ffe8b65cada4bcb6 (diff) | |
Adding informative variant of shelve_unifiable returning set of shelved evars.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions