diff options
| author | Hugo Herbelin | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:22:00 +0200 |
| commit | 50374354b7ced786d68d45884295a4c770642123 (patch) | |
| tree | 9c11b0cd9502e95ec6e296a5b1a50386dcca2eca /plugins/syntax/float_syntax.ml | |
| parent | 34237bb07fa8663d3d9e8ca4f9459f46841fd43d (diff) | |
Cleaning the use of pstate and evar_map in Search.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions