Documentation mentions non-existing symbols

[RalfJung]

In the section "Elimination principle", the docs say

Equations also automatically generates a mutually-inductive relation corre-
sponding to the graph of the programs, whose first inductive is named f_ind. It
automatically shows that the functions respects their graphs (lemma f_ind_fun)
and derives from this proof an elimination principle named f_elim.

This seems to not be correct. I cannot find neither f_ind nor f_ind_fun, only f_elim.

Here is the example code I used for testing:

From Equations Require Export Equations.

Inductive type : Type :=
  | Int
  | Bool
  | Unit
  | Fun (A B : type)
.

Equations type_size (A : type) : nat :=
  type_size Int := 1;
  type_size Bool := 1;
  type_size Unit := 1;
  type_size (Fun A B) := type_size A + type_size B + 1;
.

This prints

type_size is defined
type_size_equation_1 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_equation_1 is defined
type_size_equation_2 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_equation_2 is defined
type_size_equation_3 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_equation_3 is defined
type_size_equation_4 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_equation_4 is defined
type_size_graph is defined
type_size_graph_rect is defined
type_size_graph_rect is recursively defined
type_size_graph_correct has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_graph_correct is defined
type_size_elim has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
type_size_elim is defined
FunctionalElimination_type_size is defined
FunctionalInduction_type_size is defined

There is no type_size_ind or type_size_ind_fun.

[RalfJung]

FWIW the docs also claim that "f_unfold" is being generated, which doesn't seem to be correct either.