aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-24Merge PR #13649: Lint stdlib with -mangle-names #5coqbot-app[bot]
2020-12-21Merge PR #13651: Shorten/improve intro of "Basic proof writing" chapter.coqbot-app[bot]
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-20Merge PR #13138: Towards a documentation / cleanup of evarconvcoqbot-app[bot]
2020-12-18Merge PR #13530: Revert removal of eoi_entry in #13447coqbot-app[bot]
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
2020-12-17Merge PR #13652: Add a test for change over case nodes.coqbot-app[bot]
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
2020-12-16Merge PR #13644: Fix overlay system: projects need to be loaded before overlays.coqbot-app[bot]
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-16Merge PR #13616: Bench: add .log extension to .stdout/stderr filesPierre-Marie Pédrot
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
2020-12-15Modify Logic/JMeq.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Program/Wf.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Logic/FunctionalExtensionality.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/DecidableClass.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/CEquivalence.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/Zerob.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/IfProp.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/DecBool.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/BoolEq.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Numbers/Cyclic/Int63/Int63.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zgcd_alt.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpow_facts.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpower.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify micromega/ZMicromega.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify QArith/Qreduction.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify setoid_ring/Field_theory.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify QArith/QArith_base.v to compile with -mangle-namesJasper Hugunin
2020-12-15Catch up to where I was last time.Jasper Hugunin
2020-12-15Merge PR #13615: Document the manual tasks that I need to do at each release.coqbot-app[bot]
2020-12-15Merge PR #13625: Tweak constr_matching so as to make it tail-rec on projectio...coqbot-app[bot]
2020-12-15Merge PR #13633: [ci] uniform name of projects w.r.t. opam packagescoqbot-app[bot]
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
2020-12-15Merge PR #13621: Fast path in tclPROGRESS.coqbot-app[bot]
2020-12-15Merge PR #13632: [ci] Update pin ci scriptcoqbot-app[bot]
2020-12-15[ci] uniform name of projects w.r.t. opam packagesEnrico Tassi
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
2020-12-14Merge PR #13630: Cleanup reductionopscoqbot-app[bot]
2020-12-14Merge PR #13523: [envars] honor file "coq_environment.txt"Pierre-Marie Pédrot
2020-12-14Merge PR #13626: [ci] update doc for overlayscoqbot-app[bot]
2020-12-14Update dev/tools/pin-ci.shEnrico Tassi
2020-12-14[ci] simplify script to pin ci projectsEnrico Tassi
2020-12-14[ci] fix code to check if the overlay is validEnrico Tassi
2020-12-14Do not rely on Reductionops to recognize canonical projections.Pierre-Marie Pédrot
2020-12-14Remove most of Reductionops.*_state functions.Pierre-Marie Pédrot