aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-10Merge PR #10065: CI: run coqchk without -silentEmilio Jesus Gallego Arias
2019-05-10CI: run coqchk without -silentGaëtan Gilbert
2019-05-10Merge PR #10120: Clean-up: remove dead appveyor.sh file.Emilio Jesus Gallego Arias
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...Maxime Dénès
2019-05-09Merge PR #10126: Ignore generated dune file for Ltac2Gaëtan Gilbert
2019-05-09Ignore generated dune file for Ltac2Vincent Laporte
2019-05-09Merge PR #10082: Fix PLUGINSVO computation after ltac2 integrationMaxime Dénès
2019-05-09Merge PR #10069: Do not use the constant stack in whd_betaiota_deltazeta_for_...Hugo Herbelin
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-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ...Clément Pit-Claudel
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-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
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
2019-05-03Updating CHANGES.Hugo Herbelin
2019-05-03Merge PR #9984: Add PairUsualDecidableTypeFullThéo Zimmermann
2019-05-03Remove now useless commented codePierre Roux