Documenting check_record + changing a possibly undefined int into int option.
Tests for #3848 and #3854.
New try on Fixing an evar_map bug revealed by commit 603b66f81 on
unification flags (see also temporary revert in d083200ae5b).
Failing on unbound notation variable in notation level modifiers
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
Tentatively starting to use heuristics for evar-evar resolution: first
step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.

At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.