Removing the fv_delta field

[mtzguido]

This PR simplifies somewhat the handling of delta_depths throughout the compiler. Currently, we have an fv_delta : option delta_depth field in every fv, which is mostly set by desugaring (which is a first problem, variables created by tactics usually have this depth wrong). Also, there is a way to compute the delta_depth dynamically from the environment in Env.delta_depth_of_fv, which actually looks at the definition of the variable. But, for some identifiers, it still falls back to the fv_delta field, the reason being that using the legit delta_depth brings many regressions in the form of badly generated VCs (connectives get unfolded) or checking errors (connectives do not get unfolded when it matters, like let f : ~p = return_squash ()).

The desugarer also had a big table of assumed delta_depths, most of which were not right, but which kept the thing working. For some connectives like /\, the desugarer would set the depth to Delta_constant_at_level 1, but a conjunction created by the unifier (e.g. when meeting refinements), would use Delta_constant_at_level 0, so we were in fact mixing different depths for a same given symbol.

--

This PR removes the fv_delta field altogether, and centralizes the definition of what a delta_depth is in the typechecker (as a memoized function). Since the field is gone, the desugarer (and tactics) need not have a clue about delta_depths, so the magic tables are also now gone. This did require a patch in the unifier to handle cases like /\ above gracefully, though: when we're matching types, we do want to unfold /\ (it has a definition, we want to use it for constructive logic); but when matching propositions, such as refinement formulas, we do not. So the unifier now sets an extra flag for each problem stating whether the problem is logical or not, preventing unfolding connectives when so.

The whole thing is still not very pretty, and there are some dubious transformations like this snippet, but it's definitely cleaner and getting a consistent state that passes everest was pretty tricky, so I'd like to merge this as it is.