Merge PR #7343: Add missing index entries.

2 files changed, 28 insertions, 0 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 075235a8e2..ad7b5c82fd 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -216,6 +216,11 @@ numbers (see :ref:`datatypes`).
    Negative integers are not at the same level as :token:`num`, for this
    would make precedence unnatural.
 
+.. index::
+   single: Set (sort)
+   single: Prop
+   single: Type
+
 Sorts
 -----
 
@@ -262,6 +267,8 @@ 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 ... => ...
+
 Abstractions
 ------------
 
@@ -282,6 +289,8 @@ 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
 --------
 
@@ -320,6 +329,11 @@ The notation :n:`(@ident := @term)` for arguments is used for making
 explicit the value of implicit arguments (see
 Section :ref:`explicit-applications`).
 
+.. index::
+   single: ... : ... (type cast)
+   single: ... <: ...
+   single: ... <<: ...
+
 Type cast
 ---------
 
@@ -329,6 +343,11 @@ the type of :token:`term` to be :token:`type`.
 :n:`@term <: @type` locally sets up the virtual machine for checking that
 :token:`term` has type :token:`type`.
 
+:n:`@term <<: @type` uses native compilation for checking that :token:`term`
+has type :token:`type`.
+
+.. index:: _
+
 Inferable subterms
 ------------------
 
@@ -336,6 +355,8 @@ Expressions often contain redundant pieces of information. Subterms that can be
 automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
 guess the missing piece of information.
 
+.. index:: let ... := ... (term)
+
 .. _let-in:
 
 Let-in definitions
@@ -347,6 +368,8 @@ denotes the local binding of :token:`term` to the variable
 definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
 stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 
+.. index:: match ... with ...
+
 Definition by case analysis
 ---------------------------
 
@@ -467,6 +490,10 @@ There are specific notations for case analysis on types with one or two
 constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see
 Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
 
+.. index::
+   single: fix
+   single: cofix
+
 Recursive functions
 -------------------
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 70d46e034a..1fc267488c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -717,6 +717,7 @@ Local definitions
 Local definitions can be done as follows:
 
 .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr
+   :name: let ... := ...
 
    each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated
    by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for