aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
AgeCommit message (Expand)Author
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
2020-03-26Change logHugo Herbelin
2020-03-24“auto with zarith”: use “lia” rather than “omega”Vincent Laporte
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-03-03Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rstHugo Herbelin
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still miss...Emilio Jesus Gallego Arias
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-06[micromega] fix of bug #11191Frédéric Besson
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-16Re-implementation of zifyFrédéric Besson
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 02:41:09 +0000