diff options
| author | Pierre-Marie Pédrot | 2018-07-11 15:11:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 13:53:22 +0200 |
| commit | 270ceed48217797e99ec845cc5d1c599b5729bc2 (patch) | |
| tree | dbeb209fe008c07e020f544cd95c051c4a575145 /kernel/cClosure.mli | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
Export a wrapper simplifying the registration of vernacular commands.
Diffstat (limited to 'kernel/cClosure.mli')
0 files changed, 0 insertions, 0 deletions