Version

Coq 8.8.1

Operating system

any

Description of the problem

The manual presents a series of the examples that are supposed to demonstrate how coercions work. But it seems to me that Identity Coercion example does not do its job. Here is the snippet from the manual (I have taken the liberty of deleting some non-relevant parts):

Set Printing Coercions.
Parameters (D : nat -> bool -> Set) (E : bool -> Set).
Parameter g : forall (n:nat) (b:bool), D n b -> E b.
Coercion g : D >-> E.
Parameter T : E true -> nat.

Definition D' (b:bool) := D 1 b.
Identity Coercion IdD'D : D' >-> D.  (* Is this useless? *)
Print IdD'D.
Parameter d' : D' true.
Check (T d').

Check (T d') works the same no matter if we have Identity Coercion IdD'D or not.

What is this example supposed to show us?