Wrong documentation?

[affeldt-aist]

analysis/theories/realfun.v

Lines 14 to 15 in a5e2c65

	(* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *)
	(* continuous up to the boundary *)

@CohenCyril I remember that you recently made a comment about this documentation being wrong but I cannot find your comment. What was it?

[CohenCyril]

cf
#873 (comment)
and
#794 (comment)