From daddc14db590ce40bd528c5ee443c0e1d3c32cbb Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 8 Jun 2020 16:49:13 +0200
Subject: Merge sections on functions and function types.

---
 doc/sphinx/language/core/assumptions.rst | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 9943e0aa76..955f48b772 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -44,10 +44,11 @@ fun and forall gets identical. Moreover, parentheses can be omitted in
 the case of a single sequence of bindings sharing the same type (e.g.:
 :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`).
 
-.. index:: fun ... => ...
+.. index:: fun
+.. index:: forall
 
-Abstractions: fun
------------------
+Functions (fun) and function types (forall)
+-------------------------------------------
 
 .. insertprodn term_forall_or_fun term_forall_or_fun
 
@@ -69,11 +70,6 @@ a let-binder occurs in
 the list of binders, it is expanded to a let-in definition (see
 Section :ref:`let-in`).
 
-.. index:: forall
-
-Products: forall
-----------------
-
 The expression :n:`forall @ident : @type, @term` denotes the
 *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`.
 As for abstractions, :g:`forall` is followed by a binder list, and products
@@ -92,8 +88,8 @@ Non dependent product types have a special notation: :g:`A -> B` stands for
 :g:`forall _ : A, B`. The *non dependent product* is used both to denote
 the propositional implication and function types.
 
-Applications
-------------
+Function application
+--------------------
 
 .. insertprodn term_application arg
 
-- 
cgit v1.2.3