aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
2019-05-10Cleanup of Logic.convert_hyp.Pierre-Marie Pédrot
2019-05-10Remove ref from some implicit_discharge_requestJasper Hugunin
2019-05-10Simplify dispose_implicitsJasper Hugunin
2019-05-10Remove various circumvolutions from reduction behaviorsMaxime Dénès
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-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-10Better title for the first example of the Ltac examples section.Théo Zimmermann
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
2019-05-09Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlabMichael Soegtrop
2019-05-09Improve the first two Ltac examples.Théo Zimmermann
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 08:25:58 +0000