Update Rocq to 9.2.0

[stepchowfun]

Update the Rocq pins from 9.0.0 to rocq-core 9.2.0 and rocq-stdlib 9.1.0 (the stdlib is now versioned independently of the prover core; rocq-prover moves to its meta.1 marker version). The upgrade entails:

• Removing the Loose Hint Behavior flag, which no longer exists in 9.2, from _RocqProject and the lint commands.
• Adapting proofs in icbics.v, local_closure.v, and opening.v: the search tactic now closes goals under 9.2 that previously required manual steps, so those steps became dead code that the ! goal selector rejects.
• Importing Stdlib.Vectors.FinFun in icbics.v, since Permutation_nth moved there.
• Explicitly creating the main hint databases (regular and rewrite) in tactics.v, and generating the rewriting schemes for the tutorial's custom equality via Scheme Rewriting for eq in lesson3_logic.v — implicit creation of both is deprecated since 9.2. The generated eq_sym scheme shadows Logic.eq_sym, so one use is now qualified. The implicit-creation warnings are escalated to errors so lint-imports recognizes hint-database dependencies (this is also why kleene_data.v now requires main.tactics instead of implicitly creating the databases).
• Removing ten Require imports across nine files that the new stdlib renders unnecessary (flagged by lint-imports).

Verified locally: clean make with zero warnings, tagref, lint-general, and both lint-imports passes.

Status: Ready

Fixes: N/A

🤖 Generated with Claude Code