diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 15:21:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 15:21:19 +0200 |
| commit | 31e13998542941040343cb81787a1d7c865d5b65 (patch) | |
| tree | c8fa54eaa323e189bf19f45f0dc42e1670908b1c /interp/notation.ml | |
| parent | 1098604f599aa9aae9f07cf4960f41ef34f865e5 (diff) | |
| parent | 7ae07d738b7b2704971b8bc2becb7a1355deb5c3 (diff) | |
Merge PR #7803: [TYPO FIX] elimitate -> eliminate
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions