aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-21Add overlays.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-21Remove the artificial dependency of Heads on evaluable_global_reference.Pierre-Marie Pédrot
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-18Fixes #13657: vscoq needs goal uid.Hugo Herbelin
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
2020-12-18Do not load overlay data (workaround to fix CI).Théo Zimmermann
2020-12-18Make ssr datastructures cpattern and rpattern publicLasse Blaauwbroek
2020-12-17[ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI.Théo Zimmermann
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-16Add ounit2 to with-test dependenciesLasse Blaauwbroek
2020-12-16Add build dependency of conf-ptyon-3 to coq-docLasse Blaauwbroek
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]