#7725 (8.15): Allows overriding
intuition_solverinstead of shadowing [intuition], see also #143
#14513 (8.15): Allow
Hint Mode, inside sections.
#13952 (8.15): Use hint
#[projections(primitive=yes/no)]for better primitive projection control.
Also I removed an obsolete comment about
omega, which has been removed since Coq 8.14.