aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
2019-05-12Merge PR #10083: Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forEmilio Jesus Gallego Arias
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ...Pierre-Marie Pédrot
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10Merge PR #10058: Remove various circumvolutions from reduction behaviorsEnrico Tassi
2019-05-10Merge PR #10080: Define minimum Sphinx version in conf.py.Clément Pit-Claudel
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
2019-05-10Merge PR #10065: CI: run coqchk without -silentEmilio Jesus Gallego Arias
2019-05-10Add overlays for coq/coq#10052.Pierre-Marie Pédrot
2019-05-10Fast-path for reordering of a single closed variable.Pierre-Marie Pédrot
2019-05-10Take advantage of the ordering / conversion check split.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
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 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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 08:58:42 +0000