diff options
| author | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
| commit | 920cc6ba6ee33bf34cd853f6a9a050ed7594e2ce (patch) | |
| tree | c3874e606bdbac3bf6c3f093587e5dda8dae37ec /dev | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
| parent | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (diff) | |
Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions