diff options
| author | Théo Zimmermann | 2020-05-13 23:40:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 23:40:39 +0200 |
| commit | 0867dca735b153368c9bf258e918cf71b6761f74 (patch) | |
| tree | 353b130559afbb5c68274365d48c3b3eecf3c014 /dev/include | |
| parent | 91b5990e724acc863a5dba66acc33fd698ac26f0 (diff) | |
Extract primitive objects from Gallina ext.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions