aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-12-09Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle of...Emilio Jesus Gallego Arias
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-12-09Merge PR #10829: Section.t is never emptyPierre-Marie Pédrot
2019-12-09Merge PR #11234: [ide] Don't use -linkall for the GUI app.Pierre-Marie Pédrot
2019-12-09Merge PR #11256: [configure] [dune] Fix configure under Dune in 32bit builds.Théo Zimmermann
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-12-07[configure] [dune] Fix configure under Dune in 32bit builds.Emilio Jesus Gallego Arias
2019-12-07Merge PR #11141: Moving the diversity of constr printers to a label styleEmilio Jesus Gallego Arias
2019-12-06Adding documentation in printer.mliHugo Herbelin
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
2019-12-06Merge PR #11232: Remove latex files that should be regenerated by makeThéo Zimmermann
2019-12-06Merge PR #11174: [dune] Update to dune language version 2.0Théo Zimmermann
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Merge PR #11172: Interleave removal of coercions and search for notationsEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
2019-12-03Update doc/changelog/03-notations/11172-master+coercion-notation-interleaved-...Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03[ide] Don't use -linkall for the GUI app.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-03Merge PR #11175: coercion functions are never called without a term to coerceEnrico Tassi
2019-12-02Remove latex files that should be regenerated by makeJim Fehrle
2019-12-02Merge PR #11198: Display more information when complexity tests failHugo Herbelin
2019-12-02Merge PR #11227: Allow to override build date with SOURCE_DATE_EPOCHEmilio Jesus Gallego Arias
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02Allow to override build date with SOURCE_DATE_EPOCHBernhard M. Wiedemann
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
2019-12-02[ci] [sf] Add authentication to artifact download.Emilio Jesus Gallego Arias
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
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