| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-01-14 | Merge PR #13378: Add support for high resolution timeout functions | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2021-01-13 | Merge PR #13740: [osx] macpack also coqidetop (for libgmp) | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2021-01-13 | Merge PR #13598: [ci] window jobs based on the platform | Michael Soegtrop | |
| Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-13 | Merge PR #13675: Extrude pattern ground check | coqbot-app[bot] | |
| Reviewed-by: mattam82 | |||
| 2021-01-13 | Merge PR #13726: Use an integer indirection in UGraph | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-12 | Same treatment for pattern functions used by rewrite. | Pierre-Marie Pédrot | |
| 2021-01-12 | Extrude the check for pattern groundness outside of unification. | Pierre-Marie Pédrot | |
| 2021-01-12 | Merge PR #13742: Add a test for bound variables in match goal over a case ↵ | coqbot-app[bot] | |
| involving variables Reviewed-by: SkySkimmer | |||
| 2021-01-12 | Add an indirection to the UGraph internal representation. | Pierre-Marie Pédrot | |
| We represent entries in the graph with integers instead of levels and add a table remembering the corresponding association in the graph. | |||
| 2021-01-12 | Add a test for bound variables in match goal over a case involving variables. | Pierre-Marie Pédrot | |
| 2021-01-12 | [osx] macpack all binaries, not just coqide | Enrico Tassi | |
| 2021-01-12 | Merge PR #13704: [ci] [coq-performance-tests] Errors at end of log | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: gares | |||
| 2021-01-12 | Merge PR #13735: Add a test for a weird behaviour of tactic matching. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-12 | Merge PR #13736: Do not declare a global universe object when this set is empty. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-11 | [ci] [coq-performance-tests] Errors at end of log | Jason Gross | |
| By running `make -k; make` whenever `make` initially fails, we can get error messages to occur at the end of the log. This way they'll show up on the GitHub Actions preview/summary, rather than me having to go digging for them in the GitLab logs. | |||
| 2021-01-11 | Do not declare a global universe object when the universe set is empty. | Pierre-Marie Pédrot | |
| 2021-01-11 | Merge PR #13622: Use the Evarutil cache for Class_tactics.evar_dependencies. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-11 | Use the Evarutil cache for Class_tactics.evar_dependencies. | Pierre-Marie Pédrot | |
| 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-10 | Merge PR #13469: Use nat_or_var for fail/gfail | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Reviewed-by: ppedrot | |||
| 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 | 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |