Building CPDT with Coq 8.10.2

I’m trying to build the sources for CPDT using Coq 8.10.2.

make fails with error

File "./src/GeneralRec.v", line 890, characters 55-66:
In environment
n : nat
m : nat
The term "Ret (n + m)" has type "comp nat" while it is expected to have type
 "?T@{x:=m}" (unable to find a well-typed instantiation for
"?T": cannot ensure that "Type@{max(Set,comp.u0+1)}" is a subtype of

GeneralRec:80 reads

(** Have we finally reached the ideal solution for encoding general recursive definitions, with minimal hassle in syntax and proof obligations?  Unfortunately, we have not, as [comp] has a serious expressivity weakness.  Consider the following definition of a curried addition function: *)

Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).

This works in an earlier version of Coq I have installed.
Any hints as to what could be going wrong?