diff options
| author | Théo Zimmermann | 2020-05-13 23:59:38 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 23:59:38 +0200 |
| commit | 5e03735996709ae964c981f3bf29566dabca00bb (patch) | |
| tree | 59d7d6c76a536e081160f0513232797ce58b17e8 /doc | |
| parent | e6fca95d9b73c16e5341e47045ba2811c6bee9a7 (diff) | |
Add section on pattern matching from Gallina ext.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst (renamed from doc/sphinx/language/gallina-extensions.rst) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/extensions/match.rst index 193c799bc3..193c799bc3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/extensions/match.rst |