diff options
| author | Enrico Tassi | 2020-08-13 18:18:20 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-08-13 18:18:20 +0200 |
| commit | ca47fb67a95cf291a43a68b210b9670d4461e9d6 (patch) | |
| tree | 509fbb6f8643496489ce798b8ce05706520b5623 /plugins/syntax/string_notation.mli | |
| parent | 422e2ec9cc902bfb3f6ea78045e8490328acbd20 (diff) | |
| parent | 0c576f95fe6a804babd0ff2f296b3f112eda8ff9 (diff) | |
Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred.
Reviewed-by: gares
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions