Adding a Refine Instance Mode option that allows to deactivate the
automatic refinement of instances, thus failing when provided with
an incomplete term instead of silently lauching the proof mode.
Documenting the Set Refine Instance Mode.