aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-18Do not call the with_full_binder map variant for Reduction.instance.Pierre-Marie Pédrot
We know statically that whd_betaiota is a local reduction function, so it does not need to access the rel_context of its environment argument.
2021-01-18Move the two only calls to the strong combinator to their calling site.Pierre-Marie Pédrot
2021-01-18Move the only use of strong_with_flags to its single calling module.Pierre-Marie Pédrot
This also allows to move the strong variant of cbn to the Cbn module.
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-18Merge PR #13656: Avoid using "subgoals" in the UI, it means the same as "goals"coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: gares
2021-01-15Merge PR #13678: Cleaning up the bytecode interpreterPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-01-14Merge PR #13378: Add support for high resolution timeout functionsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-13Merge PR #13740: [osx] macpack also coqidetop (for libgmp)Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-01-13Merge PR #13598: [ci] window jobs based on the platformMichael Soegtrop
Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-13Merge PR #13675: Extrude pattern ground checkcoqbot-app[bot]
Reviewed-by: mattam82
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-13Merge PR #13726: Use an integer indirection in UGraphcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-12Same treatment for pattern functions used by rewrite.Pierre-Marie Pédrot
2021-01-12Extrude the check for pattern groundness outside of unification.Pierre-Marie Pédrot
2021-01-12Merge PR #13742: Add a test for bound variables in match goal over a case ↵coqbot-app[bot]
involving variables Reviewed-by: SkySkimmer
2021-01-12Add 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-12Add 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 coqideEnrico Tassi
2021-01-12Merge PR #13704: [ci] [coq-performance-tests] Errors at end of logcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares
2021-01-12Merge PR #13735: Add a test for a weird behaviour of tactic matching.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-12Merge 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 logJason 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-11Do not declare a global universe object when the universe set is empty.Pierre-Marie Pédrot
2021-01-11Merge PR #13622: Use the Evarutil cache for Class_tactics.evar_dependencies.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-11Use the Evarutil cache for Class_tactics.evar_dependencies.Pierre-Marie Pédrot
2021-01-11Add 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-10Merge PR #13469: Use nat_or_var for fail/gfailPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-10Remove 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-10Remove 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-10Add 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-10Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.Guillaume Melquiond
2021-01-10Remove PUSHACC0, as it is strictly equivalent to PUSH.Guillaume Melquiond
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
Reviewed-by: vbgl
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2021-01-06Merge 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-06Merge PR #13714: Changelog for 8.13.0coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-06Further 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:53:49 +0000