aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 23:56:27 +0200
committerThéo Zimmermann2020-05-13 23:56:27 +0200
commit8a35af641d92d7a65e35a3838f9cbbef4e2b2c8b (patch)
tree7b83c2477259a847b3af806fb06a5b4d858ad8d4 /doc/sphinx
parent03d36216d47e7e2d02d527f86bdcc3460c9f942d (diff)
New file on existential variables.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/language/extensions/evars.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/evars.rst
index 979a0a62e6..979a0a62e6 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/extensions/evars.rst