update reference section
commitd74ca6305b4242c643b8e7ca3e186b2156c465b0
authormartinbaker <git29f185@martinb.com>
dateFri 20 Dec 2019, 18:51 (7 years ago)
parent25af56b
docs/reference/index.rst−1
@@ -36,7 +36,6 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
3636 internals
3737 language-features
3838 language-extensions
39− elaborator-reflection
4039 type-directed-search
4140 partial-evaluation
4241 misc
docs/reference/syntax-guide.rst+1−1
@@ -83,7 +83,7 @@ users of the module being written. This can be done using ``import public``:
8383
8484.. code-block:: idris
8585
86− import public Data.Vect
86+ # import public Data.Vect
8787
8888.. _syntax-variables:
8989