aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-09Rewording, language improvements.Théo Zimmermann
2019-05-09Merge PR #10069: Do not use the constant stack in whd_betaiota_deltazeta_for_...Hugo Herbelin
2019-05-08[refman] Move all the Ltac examples to the Ltac chapter.Théo Zimmermann
2019-05-08Update release process documentation and changelog entry.Théo Zimmermann
2019-05-08Add a test that unreleased changelog of released versions is empty.Théo Zimmermann
2019-05-08Define a new `is_a_released_version` variable in configure.ml.Théo Zimmermann
2019-05-08Remove ltac2 add-on from Windows installer now that it is in the main Coq pac...Théo Zimmermann
2019-05-08Clean-up: remove dead appveyor.sh file.Théo Zimmermann
2019-05-08Merge PR #10087: Added description of QThéo Zimmermann
2019-05-08Merge PR #10086: Fix gitignore for ltac2Pierre-Marie Pédrot
2019-05-08Merge PR #10119: Show diffs in error messages only if Diffs is enabledGaëtan Gilbert
2019-05-07Show diffs in error messages only if Diffs is enabledJim Fehrle
2019-05-07Added "Recursively" for the R optionRobert Rand
2019-05-07Added description of QRobert Rand
2019-05-07Fix gitignore for ltac2Gaëtan Gilbert
2019-05-07Remove overlays for CompCert and VSTVincent Laporte
2019-05-07[nix-ci] Add coquelicot, improve flocqVincent Laporte
2019-05-07Add overlays for CompCert, VST, and coquelicotVincent Laporte
2019-05-07[Test-suite] Add output case for issue #9370Vincent Laporte
2019-05-07Improve field_simplify on fractions with constant denominatorthery
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ...Clément Pit-Claudel
2019-05-07Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forGaëtan Gilbert
2019-05-07Merge PR #10016: [test-suite] Remove a test with a Timeout that fails frequen...Vincent Laporte
2019-05-07Fix PLUGINSVO computation after ltac2 integrationGaëtan Gilbert
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaëtan Gilbert
2019-05-07Define minimum Sphinx version in conf.py.Théo Zimmermann
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
2019-05-07Merge PR #10075: [Record] Une a record to gather field declaration attributesEnrico Tassi
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
2019-05-07Merge PR #10063: CoqIDE: recognize qualified identifiers as words.Pierre-Marie Pédrot
2019-05-07Add overlays.Pierre-Marie Pédrot
2019-05-07Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-05-07[Record] DeforestationVincent Laporte
2019-05-07[Canonical structures] DeforestationVincent Laporte
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-05-06Merge PR #10068: Coqchk: encapsulating an anomaly NotConvertible into a prope...Pierre-Marie Pédrot
2019-05-06Merge PR #9964: Unreleased changelog folderVincent Laporte
2019-05-06Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.Hugo Herbelin
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
2019-05-05[make] build unreleased.rstEnrico Tassi
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
2019-05-05Merge PR #10059: Fixing bugs introduced in change_no_checkPierre-Marie Pédrot
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...Pierre-Marie Pédrot
2019-05-04Merge PR #10012: Document convert_concl_no_check (#3225)Théo Zimmermann
2019-05-04Merge PR #10057: Fix #10054: Numeral Notations without the ltac plugin.Emilio Jesus Gallego Arias
2019-05-03CoqIDE: recognize qualified identifiers as words.Jasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 23:29:38 +0000