aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-05Move universe printing out of AcyclicGraph.Pierre-Marie Pédrot
Instead we export a representation function that gives a high-level view of the data structure in terms of constraints.
2021-01-05Merge PR #13716: [doc] tell sphinxcontrib-bibtex which bibtex file to usecoqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
2021-01-05[ci] windows job based on the platformEnrico Tassi
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Add overlays.Pierre-Marie Pédrot
2021-01-04Try to preserve the old unification behaviour w.r.t. let-ins in branches.Pierre-Marie Pédrot
The infamous whd_betaiota_deltazeta_for_iota_state function is critical for unification, and it seems that eagerly reducing let-bindings appearing in case branches was a bad idea for efficiency. Instead, when try to preserve the old behaviour where a dummy beta-let cut was introduced.
2021-01-04Make detyping more robust w.r.t. case representation.Pierre-Marie Pédrot
Since we have eta-expansion guaranteed by the term representation, we do not have any more to do a little dance to try to recognize eta-expanded branches and return predicate. Still not able to compile the elpi test, but a good step towards it.
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Fix behaviour of destruct after change of case representation.Pierre-Marie Pédrot
We ensure not to generate dummy beta-cuts in case branches generated by destruct. There was seemingly code trying to perform this but in an akward way.
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-04Changelog for 8.13.0Enrico Tassi
2021-01-04[win] remove old scripts, we now use the platform onesEnrico Tassi
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
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-26Protect caml_process_pending_actions_exn with caml_something_to_do.Guillaume Melquiond
When using OCaml >= 4.10, function caml_process_pending_actions_exn is called whenever the bytecode interpreter tries to apply a term. This function exits immediately when caml_something_to_do is not set. But since term application happens every few opcodes, even exiting immediately still accounts between 5% and 10% of the whole interpreter. So, this commit makes sure the function is not called unless caml_something_to_do is already set (i.e., when the user presses Ctrl+C). This means that this conditional branch is perfectly predicted by the processor. On the following benchmark, this commit makes the VM 13% faster. Time Eval vm_compute in Pos.iter (fun x => x) tt 100000000. Note that, before OCaml 4.10, the VM code was checking the value of caml_signals_are_pending before calling caml_process_pending_signals. So, this commit actually fixes a regression.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:03:52 +0000