aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-12-06Merge PR #11232: Remove latex files that should be regenerated by makeThéo Zimmermann
Ack-by: Zimmi48
2019-12-06Merge PR #11174: [dune] Update to dune language version 2.0Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-12-05Merge PR #11172: Interleave removal of coercions and search for notationsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
Failing on CProdN([],...) was maybe a bit too radical.
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler.
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-02Remove latex files that should be regenerated by makeJim Fehrle
If these files are present in the latex directory, "make refman-pdf" may fail to generate CoqRefMan.pdf.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:41:48 +0000