fix(phl): proc rewrite /= honors the proof-local simplify context

[bgregoir]

Fixes #1145.

process_rewrite_simpl reduced with a bare EcReduction.nodelta, whose
user_local is SimplifyContext.empty. Databases activated with
hint +db and lemmas added with hint {l} — whether by the standalone
command or by the scoped with hint ... (...) form — were therefore
invisible to proc rewrite /=, unlike every other reduction tactic
(t_cbv, t_cbn, simplify, cbv), which all thread
FApi.tc1_simplify_context.

-  let ri = EcReduction.nodelta in
+  let ri =
+    { EcReduction.nodelta with
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in

The same ri is reused by the t_change discharging the side goal, so the
discharge stays consistent with the rewriting performed.

Tests

tests/procrewrite-simpl.ec gains five lemmas covering hint +db,
hint {l}, and both scoped forms. They keep the rule in a named database
so kernel conversion cannot fire it on its own, and drop the hint before
the closing apply — otherwise it is the apply's own conversion, which
does see the local context, that closes the goal, and the test passes even
with the bug present.

Checked in both directions by rebuilding: the four positive lemmas each
fail on unpatched main and pass with the patch. No regression on
procrewrite, procchange, match_codepos, local_hint_simplify,
hint_simplify_db, simplify_head_filter, simplify-delta-ops.
theories/crypto/assumptions/DHIES.ec uses the proc rewrite <pterm>
branch, which this patch does not touch.

Not included

The two related points listed at the end of the issue (ptenv_of_penv
without ~simpl:, and the absence of a use-site hint clause on
proc rewrite /=) are left out to keep this PR to the single fix.