diff options
| author | Théo Zimmermann | 2020-04-03 15:50:43 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-03 15:50:43 +0200 |
| commit | 716262faefe4ea0975eea6e125bad2dfdaaf22ba (patch) | |
| tree | 16c1ba223046a0854b7a7ffd43bc9041071208d1 /dev/base_include | |
| parent | acefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff) | |
Extract section on implicit arguments from Gallina extensions.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions