fixes #2045

[affeldt-aist]

Motivation for this change

fixes #2045

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

could you take a look at this PR @amolinamounier ?

[amolinamounier]

Is there any particular reason cst_continuous and within_continuous_cst couldn't be automatic hints as well? Looks good otherwise.

[affeldt-aist]

Is there any particular reason cst_continuous and within_continuous_cst couldn't be automatic hints as well? Looks good otherwise.

As of today, no strong reason I suspect. I think that in the past we have been cautious not to add too many hints by fear of future performance issues. We never came up with a policy regarding hints.

Regarding, cst_continuous/cst_within_continuous vs. cvg_cst/is_cvg_cst: the former is not used as much as the latter, and the latter is more primitive (in particular, {within _, continuous _} is perfectible). For these reasons, it is urgent to fix the automation of cvg_cst while cst_continuous could maybe wait and be the topic of another PR that could explore a bit more systematic way to introduce such hints (hints for obvious, dangling subgoals) and come with a principled policy for it (maybe motivated by performance measurements, using Rocq tools (see https://rocq-prover.org/doc/V9.2.0/refman/practical-tools/utilities.html#timing-targets-and-performance-testing).

[affeldt-aist]

Maybe let's merge and defer the question about cst_{within_,}continuous to an issue?