[declare] Remove recursive declaration from non-recursive functions

We move quite a few obligation functions from a `let rec ... and`
block, as they are not mutually recursive.

By the way, we perform some refactoring on `solve_by_tac`, which is
quite messy still, but now the code flow could actually accommodate
passing a declaration entry instead of low-level objects.

[It seems that we will need to introduce a special obligation entry
for that purpose, but thankfully it will be internal. We are actually
pretty close on being able to remove `build_by_tactic`, which we
should do ASAP due to its current semantics breaking abstraction
barriers]

0 files changed, 0 insertions, 0 deletions