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.
https://github.com/affeldt-aist/trajectories/blob/d7eddd45c917c1d7e628d901bd494dd2253763a5/theories/ssr_descartes/bern5.v#L88
Coq complains because
iter_natis a notation.Indeed, replacing
itern_natby, say,makes the command succeed. However, it does not seem to produce the desired
iter_nat_equationwhich is required afterwards.