diff options
| author | Théo Zimmermann | 2020-05-01 13:12:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-01 13:12:14 +0200 |
| commit | 3762e15a4a5380e03b7d0e8d6bd451ce3bf9125d (patch) | |
| tree | 08a2003f8139e60aaf471dac358f7a18c5105e9a /doc/stdlib | |
| parent | df89e28b0de6597b849078a4fd7d2dce3710f5e4 (diff) | |
Extract deprecated attribute from Gallina chapter.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions