diff options
| author | Théo Zimmermann | 2020-04-23 22:44:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-23 22:44:33 +0200 |
| commit | ac7996dbd4e6d49d7b5416b27d63b8ce9814f211 (patch) | |
| tree | 49ace6508d87c49169c28e38df3f9c9aef06e343 /kernel/nativecode.ml | |
| parent | c28eaa1067e745ce5b73e7b03162b582e9461a23 (diff) | |
| parent | 29c9d9bd47d5b8cecd6a3ce038cef4302754329f (diff) | |
Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scope
Ack-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions