TODOs in `lra`

[pi8027]

Short term:

• [x] Avoid hypotheses search triggered by exact. This can be a source of a significant slowdown.
  • Done in #74, but does not fix the slowdown.
• [x] Better error messages (things like "Cannot find witness" are shown as debug messages, which is weird).
  • Done in #75.
• [ ] Implement an option to use exact_no_check.
• [x] Support zmodType homomorphisms (additive functions) and subexpressions.
  • Done in #71.
• [x] Support nat subexpressions.
  • Done in #71.
• [ ] Support the real subset (Num.real) of any numDomainType and numFieldType.
• [ ] Reimplement vm_of_list.
• [ ] Implement a preprocessing mechanism for interval memberships.

Long term:

• [ ] For the moment, a reified term should be re-parsed by the wlra_Q or wnra_Q tactic provided by the Micromega plugin. Can we do it better? Reimplementing the witness generator as a built-in predicate of Coq-Elpi might be a solution, but it would be nice if we could do that from another Coq plugin.

[pi8027]

Better error messages (things like "Cannot find witness" are shown as debug messages, which is weird).

To do error handling properly, we have to call a witness generator (like wlra_Q) and a reflection tactic separately. But, since the former puts the witness in the context, it is unclear how to retrieve it.