Solve at least one mystery case of dangling evars.
Solve at least one mystery case of dangling evars.

At one point, ExampleMemLog.v's [log_inc_two] invoked [MEMLOG.abort]
when [MEMLOG.commit] returned false, by using [If (bool_dec ok true)].
The Hoare state, just before the [If] statement, was an OR coming from
[MEMLOG.commit_ok], consisting of two cases: either [ok = true] or [ok
= false].  This produced 4 sub-goals: the cross-product of the two ORs
from [commit_ok]'s post-condition, and the two [If] branches.

Of course, two of these [If] branches were impossible: e.g., if [ok =
true] from [commit_ok], then we cannot possibly go down the [ok = false]
branch of the [If] statement.  But SepAuto's automation machinery still
tried to cancel out the implications, creating existential variables in
the process of doing so.

After trying (and failing!) to cancel out the implications, SepAuto
invoked the [intuition] tactic, which was finally smart enough to notice
that the current hypotheses add up to [False].  Since [intuition] solved
the goal, the evars created by [cancel] never got instantiated.

Surprisingly, SepAuto.v already had a mechanisms to deal with this, by
trying to prove [False] before creating any evars in [cancel].  The only
problem is, this mechanism invoked [auto with false_precondition_hint],
but we forgot to create this database by default, making [auto] fail.
(Log.v has one example of using false_precondition_hint.)

The fix is simple: always create this (empty) hint database, because
[auto] alone is already sufficient to dismiss those two impossible
[If] cases.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl