| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-01-11 | Add a test for a weird behaviour of tactic matching. | Pierre-Marie Pédrot | |
| The arity of a destructuring let in a pattern is allowed to be shorter than the case term node it actually matches. This is an unexpected side-effect of the legacy expanded representation of cases that happens to be relied upon in the wild, as evidenced by the CI failures from #13723. | |||
| 2021-01-11 | Fix #13732: Implicit Type vs universes | Gaëtan Gilbert | |
| This returns to the previous behaviour of Implicit Type forgetting universes. `Implicit Type T : Type@{u}.` may be confusing as it is equivalent to `: Type`, but until we have a better idea of what to do with anonymous types I see no other solution, especially in the short term to fix the bug. | |||
| 2021-01-11 | Respect print_universes in detype_instance | Gaëtan Gilbert | |
| This partially fixes #13732 and matches what we do in detype_sort | |||
| 2021-01-10 | Merge PR #13469: Use nat_or_var for fail/gfail | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-01-10 | Remove MAKEPROD. | Guillaume Melquiond | |
| MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is never encountered in the fast path, this optimization is not worth the extra complexity. | |||
| 2021-01-10 | Remove SETFIELD0 and SETFIELD1. | Guillaume Melquiond | |
| The generated bytecode almost never needs to modify the field of an OCaml object. The only exception is the laziness mechanism of coinductive types. But it modifies field 2, and thus uses the generic opcode SETFIELD anyway. | |||
| 2021-01-10 | Add a peephole optimization for PUSHFIELDS(1). | Guillaume Melquiond | |
| The PUSHFIELDS opcode is a costly one, yet lots of constructors have at most one usable argument (e.g., option, nat, positive, Z, Acc). For those constructors, PUSHFIELDS(1) is replaced by GETFIELD(0);PUSH, assuming the accu register is no longer used afterwards. Replacing one single opcode by two opcodes might seem like a pessimization, but it is not. Indeed, pattern-matching branches usually start by filling the accu register with a constructor argument or the value of a free variable or a constant. All of those offer peephole optimizations for PUSH, which means that the number of opcodes actually stay constant. Note that, for the same reason, the assumption above holds in practice: the accu register is no longer used after PUSHFIELDS. | |||
| 2021-01-10 | Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused. | Guillaume Melquiond | |
| 2021-01-10 | Remove PUSHACC0, as it is strictly equivalent to PUSH. | Guillaume Melquiond | |
| 2021-01-09 | Merge PR #13299: Remember universe instances of constants in notations | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2021-01-07 | Use nat_or_var for fail/gfail | Jim Fehrle | |
| 2021-01-07 | Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵ | Pierre-Marie Pédrot | |
| at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-01-07 | Merge PR #13718: Move printing and sorting out of AcyclicGraph | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-07 | Merge PR #13715: [micromega] Add missing support for `implb` | Vincent Laporte | |
| Reviewed-by: vbgl | |||
| 2021-01-06 | Improve description of rewrite_strat/innermost and outermost | Jim Fehrle | |
| 2021-01-06 | Merge PR #13563: Revival of #9710 (Compact kernel representation of ↵ | coqbot-app[bot] | |
| pattern-matching) Reviewed-by: mattam82 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle | |||
| 2021-01-06 | Merge PR #13714: Changelog for 8.13.0 | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
| 2021-01-06 | Further pushing up the printing and sorting of universes. | Pierre-Marie Pédrot | |
| We expose the representation function in UGraph and change the printer signature to work over the representation instead of the abstract type. Similarly, the topological sorting algorithm is moved to Vernacentries. It is now even simpler. | |||
| 2021-01-06 | [micromega] Add missing support for `implb` | BESSON Frederic | |
| 2021-01-05 | Move 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-05 | Merge PR #13716: [doc] tell sphinxcontrib-bibtex which bibtex file to use | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
| 2021-01-05 | [doc] tell sphinxcontrib-bibtex which bibtex file to use | Enrico Tassi | |
| 2021-01-05 | [ci] windows job based on the platform | Enrico Tassi | |
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
| 2021-01-04 | Document the change of case representation. | Pierre-Marie Pédrot | |
| 2021-01-04 | Add overlays. | Pierre-Marie Pédrot | |
| 2021-01-04 | Try 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-04 | Make 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-04 | Remove redundant univ and parameter info from CaseInvert | Gaëtan Gilbert | |
| 2021-01-04 | Fix 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-04 | Temporarily 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-04 | EConstr iterators respect the binding structure of cases. | Pierre-Marie Pédrot | |
| Fixes #3166. | |||
| 2021-01-04 | Change 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-04 | Move 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-04 | Merge PR #13685: Add a debug printer for fconstr substitutions. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-04 | Merge PR #13694: Add a test for a complex conversion involving ↵ | coqbot-app[bot] | |
| pattern-matching with let-bindings Reviewed-by: SkySkimmer | |||
| 2021-01-04 | Changelog for 8.13.0 | Enrico Tassi | |
| 2021-01-04 | [win] remove old scripts, we now use the platform ones | Enrico Tassi | |
| 2021-01-02 | Deprecate "at ... with ..." in change tactic | Jim Fehrle | |
| (use "with ... at ..." instead) | |||
| 2021-01-01 | Merge PR #13470: Convert rewriting and proof-mode chapters to prodn | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: JasonGross | |||
| 2021-01-01 | Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-31 | Adding a test for conversion involving let-bindings in inductive parameters. | Pierre-Marie Pédrot | |
| 2020-12-31 | Add a test for a complex conversion involving pattern-matching with ↵ | Pierre-Marie Pédrot | |
| let-bindings. | |||
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-12-30 | Merge PR #13692: Fix failing Windows CI builds. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-30 | Merge PR #13321: Move evaluable_global_reference from Names to Tacred. | coqbot-app[bot] | |
| Reviewed-by: herbelin Ack-by: ejgallego | |||
| 2020-12-30 | Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783). | coqbot-app[bot] | |
| Reviewed-by: herbelin | |||
| 2020-12-30 | Fix 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-30 | Merge PR #13684: Document the -native-compiler option | coqbot-app[bot] | |
| Reviewed-by: silene Ack-by: Zimmi48 Ack-by: jfehrle | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |