aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-12-01Merge PR #11220: coq_makefile: ml4 -> mlg in usage (since ml4 files are rejec...Enrico Tassi
2019-11-30coq_makefile: ml4 -> mlg in usage (since ml4 files are rejected).Hugo Herbelin
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-29Merge PR #11184: Undeprecate Add Setoid / Add Morphism.Pierre-Marie Pédrot
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
2019-11-29Merge PR #11204: Relax the pattern complexity testEmilio Jesus Gallego Arias
2019-11-29Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` optionPierre-Marie Pédrot
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
2019-11-28Merge PR #11192: [ci] Split up fiat-crypto depsEmilio Jesus Gallego Arias
2019-11-28Merge PR #11197: Release notes for Coq 8.10.2Théo Zimmermann
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-28Fix extension of changelog file.Théo Zimmermann
2019-11-28Relax the pattern complexity testJason Gross
2019-11-27Merge PR #11187: Remove deprecated commands `AddPath`, `AddRecPath` and `DelP...Emilio Jesus Gallego Arias
2019-11-27remove *.vos and *.vok file in "make clean"Olivier Laurent
2019-11-27Merge PR #11199: Correcting unintended changelog message for #11090 (coercion...Théo Zimmermann
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
2019-11-27[ci] List build:edge+flambda in depsJason Gross
2019-11-27[ci] Split out the dependencies of fiat-cryptoJason Gross
2019-11-27[ci] Build slightly more in the fiat-crypto targetJason Gross
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation regress...Hugo Herbelin
2019-11-27Merge PR #11158: [release] Update files for 8.12 release per release process.Théo Zimmermann
2019-11-27Display more information when complexity tests failJason Gross
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11196: missing " in CONTRIBUTING.mdThéo Zimmermann
2019-11-27missing "Olivier Laurent
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ...Pierre-Marie Pédrot
2019-11-27Merge PR #11193: weaker then -> weaker thanThéo Zimmermann
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
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-26Remove some trailing whitespace in theories/Program/Tactics.vJason Gross
2019-11-26Merge PR #11179: Fix Windows 32 bit buildEmilio Jesus Gallego Arias
2019-11-26Update test-suite/complexity/pattern.vJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11180: Add more development setup instructions for tutorialsEmilio Jesus Gallego Arias
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
2019-11-26Fix Windows 32 bit buildPierre Roux
2019-11-26coercion functions are never called without a term to coerceGaëtan Gilbert