This is a minor update of Equations, now compatible with Coq 8.20. The main changes are fixes in the funelim
tactic and simplification engine to avoid trying to simplify unrelated hypotheses (those under "block" markers). which sometimes led to slowing down the tactic.
Also includes performance improvements by @ppedrot.
What's Changed
- Remove a useless evar normalization in Equations.define_by_eqs. by @ppedrot in #579
- Adapt to coq/coq#18327 (projection opacity) by @rlepigre in #574
- Adapt to coq/coq#18603 (print_rel_context takes evar map) by @SkySkimmer in #581
- Adapt to coq/coq#18224 by @proux01 in #578
- Don't pierce Qed in debug message (adapt to coq/coq#18422) by @SkySkimmer in #586
- Adapt to coq/coq#18546. by @rlepigre in #582
- Adapt to coq/coq#18864 (search_guard can handle evars) by @SkySkimmer in #587
- Adapt w.r.t. coq/coq#18911. by @ppedrot in #588
- Adapt w.r.t. coq/coq#18935. by @ppedrot in #590
- Adapt to coq/coq#18938 (EConstr.ERelevance) by @SkySkimmer in #591
- Use correct scheme kind in example by @SkySkimmer in #594
- Adapt to Coq PR #18743: search_guard is now able to decide late if a recursive definition is a fix or a cofix by @herbelin in #584
- Fix
simplify
breaking the transparency/opaque status of constants a… by @mattam82 in #593 - Centralize the use of Tactics.assert_before_replacing. by @ppedrot in #601
- Revert "Fix
simplify
breaking the transparency/opaque status of constants a…" by @mattam82 in #603 - Fix funelim and add a
funelim_nosimp
variant which does not try to … by @mattam82 in #604 - Replace the outdated "Below" hint database with a
rec_decision
data… by @mattam82 in #602 - Adapt to Coq PR #18795 (more uniform API for declare.ml) by @herbelin in #599
- Adapt w.r.t. coq/coq#19120. by @ppedrot in #605
- Remove a good part of the sources of abusive typing by @ppedrot in #606
- Turn context_map into a record. by @ppedrot in #607
- Enforce more static typing by @ppedrot in #608
- Adapt w.r.t. coq/coq#19313. by @ppedrot in #611
- adapt to coq/coq#19300 by @gares in #610
Full Changelog: v1.3-8.19...v1.3.1-8.20