refactor(pl): inline as program transformations

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the inline tactic class onto
the transformation rule of each logic:

• rules/transforms/ecTrInline.ml: a new catalogue entry inline,
  whose parameters are resolved: the calls to inline are selected by a
  pattern of integer offsets (possibly nested in the branches of an
  if, a while or a match), plus the tuple flag. Each selected
  call x <- f(es) becomes the assignment of the arguments to fresh
  copies of the parameters, the body of f with its parameters and
  locals renamed to fresh program variables (added to the memory), and
  the assignment of the result (component-wise, through fresh
  variables, for a tuple pattern without tuple). No obligation. The
  entry checks itself that each selected f is concrete, that, for a
  call in a loop body, f never reads a local before writing it (same
  messages as before), and that the pattern matches the statement.
• The inline tactic is derived in every logic where it exists
  (hoare, ehoare, bdhoare, equiv one side at a time): it resolves the
  calls as before (by name / all, occurrences, code position) and
  applies t_<logic>_transform with the entry. The derived tactic is
  one line per logic, so it stays in ecPhlInline.ml, next to the
  resolution and the elaboration, instead of one module per logic.
• ecPhlInline.ml: the pattern type is re-exported from the entry, the
  t_inline_* functions are adapters onto the transformation rules
  (no more xmutate1 nor t_low* wrappers); its interface is
  unchanged.
• REFACTORING.md, README.md, EcPlTransform: the catalogue lists inline.

Behaviour is preserved: same goals and error messages in every logic
and on both equiv sides. The only difference is unreachable from the
surface syntax: an ill-formed pattern passed to t_inline_* from
OCaml now fails with "invalid inlining pattern" instead of an
assertion failure.

Validation: new test tests/inline.ec (every form, every logic, both
equiv sides, nested positions, error paths), passing with the
reference build and this one under EC_RECHECK=1, with identical goals
and error messages at each step; stdlib, unit and examples under
EC_RECHECK=1, zero RecheckFailure. Each <logic>-transform checker,
when broken on the inline entry only, is caught only under
EC_RECHECK, on the new test and on the stdlib / unit files using it
(failing files): hoare 8 / 3, ehoare 0 / 1, bdhoare 10 / 1, equiv
27 / 6.