aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-21Merge PR #13651: Shorten/improve intro of "Basic proof writing" chapter.coqbot-app[bot]
Reviewed-by: jfehrle
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
It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
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]
Reviewed-by: gares
2020-12-18Merge PR #13530: Revert removal of eoi_entry in #13447coqbot-app[bot]
Reviewed-by: herbelin
2020-12-18Fixes #13657: vscoq needs goal uid.Hugo Herbelin
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: gares Ack-by: SkySkimmer
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]
Reviewed-by: SkySkimmer
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
This is extracted from #13563.
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
This will help with reproducibility for people who have something in their coqrc file. Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-16Merge PR #13644: Fix overlay system: projects need to be loaded before overlays.coqbot-app[bot]
Reviewed-by: gares
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-16Merge PR #13616: Bench: add .log extension to .stdout/stderr filesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
Also fixes is_in_projects
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
Many of the changes are a consequence of coq/coq#13132.
2020-12-15Merge PR #13615: Document the manual tasks that I need to do at each release.coqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13625: Tweak constr_matching so as to make it tail-rec on ↵coqbot-app[bot]
projection expansion. Reviewed-by: ejgallego
2020-12-15Merge PR #13633: [ci] uniform name of projects w.r.t. opam packagescoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
Reviewed-by: herbelin
2020-12-15Merge PR #13621: Fast path in tclPROGRESS.coqbot-app[bot]
Reviewed-by: herbelin
2020-12-15Merge PR #13632: [ci] Update pin ci scriptcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-15[ci] uniform name of projects w.r.t. opam packagesEnrico Tassi
This makes it easier to track projects across Coq's CI and the platform
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-14Merge PR #13630: Cleanup reductionopscoqbot-app[bot]
Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:07:34 +0000