diff options
| author | Matthieu Sozeau | 2018-08-15 14:22:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:14:10 +0100 |
| commit | 2cf15ef8e3ddebe285ec0e9f5f8715b025ba4eec (patch) | |
| tree | 4d4e075161b3d54e7fd49ed90d830f2e478aac6e /plugins | |
| parent | af9b88c253b578ad53ee884ff3102d0a74056a1e (diff) | |
Rename types_or_terms and the unification function types
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions