This release ports Equations to Rocq 9.2 and features: performance improvements by @ppedrot support for goal names from evar/hole names and new [obligations] attribute https://github.com/mattam82/Coq-Equations/pull/695 by @mattam82 What's Changed Adapt to rocq-prover/rocq#20781. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/657 Adapt to rocq-prover/rocq#20902 (elimination_suffix moved) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/659 Adapt to rocq-prover/rocq#20614 (induction finds schemes through register) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/662 Adapt to rocq-prover/rocq#21110. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/663 Adapt to rocq-prover/rocq#21097 (Use einstance everywhere)) by @yannl35133 in https://github.com/mattam82/Coq-Equations/pull/664 Adapt to rocq-prover/rocq#20506 by @jrosain in https://github.com/mattam82/Coq-Equations/pull/652 Adapt to rocq-prover/rocq#21254 (stop catching async exceptions) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/666 Fix deprecations in master by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/668 Adapt to rocq-prover/rocq#21281 (printing flags passed functionally) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/669 Adapt to rocq-prover/rocq#21380. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/672 Adapt to rocq-prover/rocq#21195 (parsing of elim constraints) by @jrosain in https://github.com/mattam82/Coq-Equations/pull/670 Adapt to rocq-prover/rocq#21391. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/674 Adapt to rocq-prover/rocq#21381. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/673 Fix deprecations in master by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/677 Fix 667 by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/678 Adapt to rocq-prover/rocq#21394. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/675 Nix Config by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/679 Clean enter_goal API, not providing a gl handle by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/680 Adapt to rocq-prover/rocq#21384. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/676 Adapt to rocq-prover/rocq#21395 (revert univ_decl name change) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/681 Adapt to Rocq PR#21419 by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/682 Adapt to rocq-prover/rocq#21426. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/683 Adapt to rocq-prover/rocq#21366. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/671 Adapt to rocq-prover/rocq#21431 (Stop using Evd.universe_rigidity) by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/684 Fix hott build by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/685 Adapt to rocq-prover/rocq#21486. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/686 Stop pushing proof-local qualities in the global environment. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/687 Share typing of mutual definitions. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/689 Do not perform guard checking when inferring universe constraints. by @ppedrot in https://github.com/mattam82/Coq-Equations/pull/691 Add new attribute [obligations] and global [Set Equations Obligations] by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/695 Fix rocqdep warnings by @SkySkimmer in https://github.com/mattam82/Coq-Equations/pull/692 Support goal names from evar names in the term by @mattam82 in https://github.com/mattam82/Coq-Equations/pull/697 New Contributors @yannl35133 made their first contribution in https://github.com/mattam82/Coq-Equations/pull/664 Full Changelog: https://github.com/mattam82/Coq-Equations/compare/v1.3.1-9.1...v1.3.2-9.2