aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
2021-01-18Adding changelog for #13512.Hugo Herbelin
2021-01-18Adding overlay for perennial.Hugo Herbelin
2021-01-18Preventing internal temporary names to impact the "?H"-like intro-pattern names.Hugo Herbelin
2021-01-18Further simplifications in intro_patterns machinery.Hugo Herbelin
2021-01-18Small reworking of code in intros-pattern.Hugo Herbelin
We compute earlier if "apply in" clears or not. We inline prepare_naming into its only client prepare_intros_opt (using the more general make_naming instead).
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
We build earlier the final expected name at the end of a sequence of "%" introduction patterns.
2021-01-18Merge PR #13454: Remove unused retro_reflPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-01-18Merge PR #13723: Use a compact case representation for patternscoqbot-app[bot]
Reviewed-by: mattam82
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
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-18Add changelogPierre Roux
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
Also works for simpl.
2021-01-18Print primitive constants in debugerPierre Roux
This was raising a Not_found exception due to the unknown scope.
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:44:51 +0000