Make dependent elimination compatible with Set Mangle Names

[thomas-lamiaux]

Fixes #733.

Under Set Mangle Names, dependent elimination ... as [pat] did not bind the pattern names, and both it and depelim/noconf mangled the names of the pre-existing hypotheses they revert and reintroduce, making proofs using them impossible to write in a mangle-robust way (unlike inversion ... as).

Root cause

The covering contexts already carry the intended binder names: user-given names are installed verbatim by Covering.rename_domain, and generated names are freshened (and mangled, when the option is set) by the covering engine itself. The names are lost at the very last step: when the subgoal evars are created, Evarutil.push_rel_context_to_named_context regenerates every hypothesis name through Namegen.next_ident_away, which applies mangle_id indiscriminately — binder names carry no user/generated provenance, so Rocq cannot tell them apart. By contrast, inversion/destruct introduce their hypotheses in the existing named context with NamingMustBe-style intros, which bypass name generation.

Fix

• depelim.ml: after refining with the covering term, rename the hypotheses of each subgoal back to the binder names of the corresponding covering context. The mapping is collected from the Compute leaves of the splitting tree: each leaf's evar instance aligns its (mangled) named context with the covering rel context positionally. In the default mode this is a no-op, since the evar naming reuses the binder names. The surrounding-context patterns of the generated clauses are also marked Implicit rather than Generated so their names are preserved by rename_domain.
• covering.ml: name priority User > Implicit > Generated: an explicit pattern name takes priority over an implicitly named variable (e.g. a preexisting hypothesis name) both when binding pattern variables and in the shadowing check, and rename_domain drops Implicit bindings whose name is already taken instead of producing duplicate hypothesis names. (Without this, e.g. HoTT_light.v's dependent elimination b as [(a, 1)] with a := x in the context would fail.)
• context_map.ml: context_map_to_lhs ~keep_names reuses context binder names verbatim for variable patterns, used by pattern-less dependent elimination so that the unrelated hypotheses keep their names while the fresh constructor arguments still get mangled ones.
• extra_tactics.ml / CoreTactics.v: new intro_binder_name tactic that introduces the next hypothesis reusing its binder name verbatim (subscript-freshened, never mangled); intros_until_block now uses it, which fixes the Ltac-based depelim/noconf/dependent induction pipeline that reverts the telescope behind a block and reintroduced it with plain intro.

Generated names remain mangled as the option intends; only names the user wrote (as-patterns or existing hypothesis names) survive.

Testing

• New test-suite/issue733.v covering all the issue's scenarios plus noconf.
• Full build (theories, examples including HoTT_light.v) and test-suite pass.

🤖 Generated with Claude Code