aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: silene
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-12-01Merge PR #11220: coq_makefile: ml4 -> mlg in usage (since ml4 files are ↵Enrico Tassi
rejected). Reviewed-by: gares
2019-11-30coq_makefile: ml4 -> mlg in usage (since ml4 files are rejected).Hugo Herbelin
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
Fixes #10573
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
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
Reviewed-by: ppedrot
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
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
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-29Merge PR #11204: Relax the pattern complexity testEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-29Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` optionPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
This lets us get rid of dummy proofview manips. Simplifications based on [(tclUNIT foo >>= f) = f foo]
2019-11-28Merge PR #11192: [ci] Split up fiat-crypto depsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-28Merge PR #11197: Release notes for Coq 8.10.2Théo Zimmermann
Reviewed-by: Zimmi48
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
Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now.
2019-11-28Fix extension of changelog file.Théo Zimmermann
2019-11-28Relax the pattern complexity testJason Gross
c.f. discussion at https://github.com/coq/coq/pull/11177#issuecomment-559139477
2019-11-27Merge PR #11187: Remove deprecated commands `AddPath`, `AddRecPath` and ↵Emilio Jesus Gallego Arias
`DelPath` Reviewed-by: ejgallego
2019-11-27remove *.vos and *.vok file in "make clean"Olivier Laurent
2019-11-27Merge PR #11199: Correcting unintended changelog message for #11090 ↵Théo Zimmermann
(coercion+notation regression) Reviewed-by: Zimmi48
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
Fixes #10576
2019-11-27[ci] List build:edge+flambda in depsJason Gross
Quoting Gaëtan Gilbert from gitter: > IIRC dependencies is for artifacts, and the path in the immediate dep > grabs all the user-contrib stuff so you don't need to list the > transitive dependencies, but you do need to list the base build since > it's not in user contrib > this stuff isn't necessarily done intentionally though
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
This adds a couple extra files, but not many.
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation ↵Hugo Herbelin
regression).
2019-11-27Merge PR #11158: [release] Update files for 8.12 release per release process.Théo Zimmermann
Reviewed-by: Zimmi48
2019-11-27Display more information when complexity tests failJason Gross
In particular, display how long they took in bogomips-adjusted centiseconds.
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
Reviewed-by: Zimmi48
2019-11-27missing "Olivier Laurent
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ↵Pierre-Marie Pédrot
universes Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-11-27Merge PR #11193: weaker then -> weaker thanThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
Reviewed-by: herbelin
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.
2019-11-26Make rapply handle all numbers of underscoresJason Gross
Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual
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
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: erikmd Ack-by: silene
2019-11-26Update test-suite/complexity/pattern.vJason Gross
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a ↵Emilio Jesus Gallego Arias
refined version of #8890 which prevents #11033. Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-11-26Merge PR #11180: Add more development setup instructions for tutorialsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-26Fix Windows 32 bit buildPierre Roux
2019-11-26coercion functions are never called without a term to coerceGaëtan Gilbert
(inh_conv_coerces_to is unused so we remove it) This makes the code simpler, removing dead match branches and Option.maps/gets
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 17:12:37 +0000