aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-03Update ↵Hugo Herbelin
doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
We renounce to the ad hoc rule preferring a notation w/o delimiter for a term with coercions stripped over a notation for the fully-applied terms with coercions not removed. Instead, we interleave removal of coercions and search for notations: we prefer a notation for the fully applied term, and, if not, try to remove one coercion, and try again a notation for the remaining term, and if not, try to remove the next coercion, etc. Note: the flatten_application could be removed if prim_token were able to apply on a prefix of an application node.
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
Reviewed-by: JasonGross Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-03Merge PR #11175: coercion functions are never called without a term to coerceEnrico Tassi
Reviewed-by: gares
2019-12-02Merge PR #11198: Display more information when complexity tests failHugo Herbelin
Reviewed-by: gares Reviewed-by: herbelin
2019-12-02Merge PR #11227: Allow to override build date with SOURCE_DATE_EPOCHEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-12-02Allow to override build date with SOURCE_DATE_EPOCHBernhard M. Wiedemann
in order to make builds reproducible. See https://reproducible-builds.org/ for why this is good and https://reproducible-builds.org/specs/source-date-epoch/ for the definition of this variable. Fixes #11037
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Merge PR #11165: [CI] Test latest artifacts of SF instead of the stable versionEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-12-02[ci] [sf] Add authentication to artifact download.Emilio Jesus Gallego Arias
It seems we need to pass the token to the actual artifact download.
2019-12-02[CI] Test latest artifacts of SF instead of the stable versionMaxime Dénès
2019-12-02Merge PR #11031: Release notes 8.11Pierre-Marie Pédrot
2019-12-02List of 8.11 contributors and stats.Théo Zimmermann
2019-12-02Merge redundant consecutive changelog entries on reals.Théo Zimmermann
2019-12-02Highlight refine attribute for Instance.Théo Zimmermann
2019-12-02Warn more clearly about incompatibilities coming from #10476.Théo Zimmermann
2019-12-028.11 release notes.Matthieu Sozeau
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:16:39 +0000