aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-13Merge PR #13598: [ci] window jobs based on the platformMichael Soegtrop
Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
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-12Restore the corner-case behaviour for let-bound variables in patterns.Pierre-Marie Pédrot
2021-01-12Slight tweak of the matching algorithm for PIf vs. Case.Pierre-Marie Pédrot
It is equivalent but makes the code more similar to the PCase vs. Case case (aha).
2021-01-12Change the case representation of patterns.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-11Make sure Ltac2 get cleaned too.Guillaume Melquiond
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-11Fix #13732: Implicit Type vs universesGaë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-11Respect print_universes in detype_instanceGaëtan Gilbert
This partially fixes #13732 and matches what we do in detype_sort
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-08Modify Structures/OrderedType.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Structures/DecidableType.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/SetoidDec.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/SetoidClass.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Lists/SetoidList.v to compile with -mangle-namesJasper Hugunin
I used `match goal` a lot to access hypotheses without knowing their name.
2021-01-08Modify Sorting/Sorted.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/EquivDec.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Program/Subset.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Logic/ProofIrrelevanceFacts.v to compile with -mangle-namesJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:56:46 +0000