diff options
| author | Pierre-Marie Pédrot | 2019-07-29 13:13:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-29 13:13:58 +0200 |
| commit | e34fe0ab41143817f8dfd465ba18eaa6039b3c2f (patch) | |
| tree | 98d5fbbd8c65e77a43c5a4218e1b4b3e510a7d8f /gramlib | |
| parent | bbec12e3bb2cd1062bd833bbb2c44adbeef33503 (diff) | |
| parent | e9a6a3115d801140663c15341662918d9645681c (diff) | |
Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.
Reviewed-by: ppedrot
Diffstat (limited to 'gramlib')
0 files changed, 0 insertions, 0 deletions