Functional Scheme

[affeldt-aist]

https://github.com/affeldt-aist/trajectories/blob/d7eddd45c917c1d7e628d901bd494dd2253763a5/theories/ssr_descartes/bern5.v#L88

Coq complains because iter_nat is a notation.
Indeed, replacing itern_nat by, say,

Definition iter_nat (n : nat) {A : Type} (f : A -> A) (x : A) : A :=
  nat_rect (fun _ => A) x (fun _ => f) n.

makes the command succeed. However, it does not seem to produce the desired
iter_nat_equation which is required afterwards.

[ybertot]

bern5.v is not central in the development. This is a low priority issue.