aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-04Temporarily deactivating printing check for cases.Pierre-Marie Pédrot
Destruct has changed semantics, but I'd like to see how CI fares so far.
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
Fixes #3166.
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2021-01-04Move the relative linking order of Inductive w.r.t. VM / native.Pierre-Marie Pédrot
We need this file for the upcoming kernel representation change there.
2021-01-04Merge PR #13685: Add a debug printer for fconstr substitutions.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-04Merge PR #13694: Add a test for a complex conversion involving ↵coqbot-app[bot]
pattern-matching with let-bindings Reviewed-by: SkySkimmer
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-01-01Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3.coqbot-app[bot]
Reviewed-by: gares
2020-12-31Adding a test for conversion involving let-bindings in inductive parameters.Pierre-Marie Pédrot
2020-12-31Add a test for a complex conversion involving pattern-matching with ↵Pierre-Marie Pédrot
let-bindings.
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-30Merge PR #13692: Fix failing Windows CI builds.coqbot-app[bot]
Reviewed-by: gares
2020-12-30Merge PR #13321: Move evaluable_global_reference from Names to Tacred.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: ejgallego
2020-12-30Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783).coqbot-app[bot]
Reviewed-by: herbelin
2020-12-30Fix failing Windows CI builds.Théo Zimmermann
Following a recent change in Cygwin. Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2020-12-30[ci] Switch to testing the maintenance branch for Flocq 3.Théo Zimmermann
This is the version that CompCert will be compatible with for the time being.
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
Reviewed-by: silene Ack-by: Zimmi48 Ack-by: jfehrle
2020-12-29Merge PR #13686: [refman] Clarify meaning of goal in documentation of ↵coqbot-app[bot]
instantiate. Reviewed-by: jfehrle
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-28Register a printer for fconstr substitutions in the kernel.Pierre-Marie Pédrot
2020-12-28Export a high-level representation of term substitutions.Pierre-Marie Pédrot
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: palmskog
2020-12-28Merge PR #13662: Fixes #13657: vscoq needs goal uid.coqbot-app[bot]
Reviewed-by: gares
2020-12-28Fix broken HTML rendering of inference rules (fix #12783).Guillaume Melquiond
2020-12-27Merge PR #13659: Make ssr datastructures cpattern and rpattern publiccoqbot-app[bot]
Reviewed-by: gares
2020-12-27Merge PR #13677: CoqIDE: Fix CC reference in makefilecoqbot-app[bot]
Reviewed-by: gares
2020-12-27Refactor cpattern into a recordLasse Blaauwbroek
2020-12-27Make ssrtermkind algebraic instead of a charLasse Blaauwbroek
2020-12-27CoqIDE: Fix CC reference in makefileMichael Soegtrop
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-26Merge PR #13650: [ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI.coqbot-app[bot]
Reviewed-by: gares Ack-by: MSoegtropIMC
2020-12-25Merge PR #13673: Clean ALL sphinx output filescoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-24Clean ALL sphinx output filesJim Fehrle
2020-12-24Merge PR #13649: Lint stdlib with -mangle-names #5coqbot-app[bot]
Reviewed-by: anton-trunov
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:30:39 +0000