CodyWaite example fails on interval tactic (not only syntax)
Working on a "smoke test kit" for the Coq Platform I found that the CodyWaite example does not work any more with Coq 8.13, Interval 4.1 and Flocq 3.3.1. One thing is the Require and the option syntax change, but when I fix this i get with interval_intro nowhere close to what shall be proved (quite a few orders of magnitude off). It looks like a regression in Interval to me.