aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 20:02:37 +0200
committerThéo Zimmermann2020-05-13 20:02:37 +0200
commita403808cc4151242ec64d63df63b27128c539191 (patch)
treedb7e7037c6f8fb7d3e17b9d8e6c0dd38cc79d2c3 /doc
parentd3ad26c8f2b53f3101338f3764ccb54eb0177c3a (diff)
Create new file on Inductive types.
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/core/inductive.rst (renamed from doc/sphinx/language/gallina-specification-language.rst)0
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/core/inductive.rst
index b64c0aea95..b64c0aea95 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/core/inductive.rst