aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
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-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-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-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-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-26Remove undocumented and deprecated `Congruence Depth` optionMaxime Dénès
It was a no-op.
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
and do not run template_candidate in the upper layers when the template attribute is given. This means we can use an over-approximation in the upper layer implementation of template_candidate (returning false even in cases which the kernel may accept) if we ever want to.
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-26Merge PR #11173: [ssr] fix «W -- weakening» docEnrico Tassi
Reviewed-by: gares
2019-11-26Merge PR #11034: Update update-compat.pyThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-25Add more development setup instructions for tutorialsTalia Ringer
2019-11-25Error fatally if update-compat.py gets no flagJason Gross
c.f. https://github.com/coq/coq/pull/11032#issue-335944369 Also, change the default from python2 to python3 for update-compat while we're at it, and update file unicode handling accordingly. (Note that this file still works with both python2 and python3.)
2019-11-25Merge PR #11159: Minor fix in doc for [unfold]Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
Close #9634
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-25Nsatz: use “lia” rather than “omega”Vincent Laporte
2019-11-25setoid_ring: do not use “omega”Vincent Laporte
2019-11-25zify: explicitly use “lia”Vincent Laporte
2019-11-25btauto: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutEq: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutSetoid: use “lia” rather than “omega”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:42:20 +0000