aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-14Merge PR #13523: [envars] honor file "coq_environment.txt"Pierre-Marie Pédrot
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: herbelin Ack-by: ppedrot
2020-12-14Merge PR #13626: [ci] update doc for overlayscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-14Update dev/tools/pin-ci.shEnrico Tassi
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-12-14[ci] simplify script to pin ci projectsEnrico Tassi
2020-12-14[ci] fix code to check if the overlay is validEnrico Tassi
2020-12-14Do not rely on Reductionops to recognize canonical projections.Pierre-Marie Pédrot
No need to call the whole whd_gen machinery when a simple matching over a term would suffice. Note that this changes a bit the semantics, but I suspect that the previous code was buggy. Indeed, whd_nored also pushes cases and fixpoints on the stack, so that an applied canonical projection inside such a context would also match. But the caller in unification performs an approximate check where the term needs to be an application or a projection, which would prevent such complex situations most of the time, e.g. it would work with a dummy commutative cut but not their corresponding vanilla match.
2020-12-14Remove most of Reductionops.*_state functions.Pierre-Marie Pédrot
There functions export the internal stack representation. The only real user is unification, which is suffering from major performance issues due to the naive representation of substitutions in processes.
2020-12-14Reuse the cache everywhere possible in Clenv.Pierre-Marie Pédrot
2020-12-14Store the metasubst cache in clenvs.Pierre-Marie Pédrot
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-12-14Cache meta access in meta_instance.Pierre-Marie Pédrot
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-14Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction ↵Pierre-Marie Pédrot
Pattern Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-12-13Update dev/ci/user-overlays/README.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-13Merge PR #13619: doc: Clarify the status of simpl vs cbncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-13Add changelog for #13509.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-13Removing unused internal introduction-patterns flag assert_style.Hugo Herbelin
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-12Merge PR #13620: Use a registered printer for tactic coercion failure.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: herbelin
2020-12-12[ci] update doc for overlaysEnrico Tassi
2020-12-12Tweak constr_matching so as to make it tail-rec on projection expansion.Pierre-Marie Pédrot
This was revealed on the rewriter contrib with the compact-case-repr branch.
2020-12-12Small API encapsulation inside Redexpr.Pierre-Marie Pédrot
We move bind_red_expr_occurrences from Tactics to Redexpr, where it semantically belongs. We also hide it and seal the corresponding evaluated types.
2020-12-12Extrude the computation of redexp flags in reduce.Pierre-Marie Pédrot
This was a source of slowdown observed in bedrock2.
2020-12-12Split the intepretation of red_exprs in two phases.Pierre-Marie Pédrot
2020-12-12Generalize the type of red_expr w.r.t. the type of flags they contain.Pierre-Marie Pédrot
2020-12-12Merge PR #13603: [ci] function to declare projectscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: RalfJung Ack-by: Zimmi48
2020-12-11Revert removal of eoi_entry in #13447Jim Fehrle
2020-12-11Merge PR #13492: Removing non relevant argument binding_kind of GLocalDef.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-11Fast path in tclPROGRESS.Pierre-Marie Pédrot
We first check that the list of goals have the same length before trying to engage into potentially costly equality checks.
2020-12-11Use a registered printer for tactic coercion failure.Pierre-Marie Pédrot
Otherwise we pay a high cost for printing that might never make it to the user.
2020-12-11doc: Clarify the status of simpl vs cbnClément Pit-Claudel
The cbn tactic was documented in aa9db490a2. The current manual causes confusion by suggesting that cbn is a replacement for simpl, while in practice they do different things, both with their own quirks. Given that neither is consistently faster than the other, I think it's worth clarifying the manual.
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: proux01 Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-12-11Merge PR #13611: Clarify changelog categories.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-12-11Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 ↵Clément Pit-Claudel
release. Reviewed-by: cpitclaudel
2020-12-11Merge PR #13540: Clean support of primitive integersPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: proux01
2020-12-11Bench: add .log extension to .stdout/stderr filesGaëtan Gilbert
Hopefully this allows viewing online with a download dialog on gitlab.
2020-12-11Document the manual tasks that I need to do at each release.Théo Zimmermann
2020-12-11Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds ↵coqbot-app[bot]
forall Reals. Reviewed-by: thery
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-11Bump reference to 8.12 refman following unexpected 8.12.2 release.Théo Zimmermann
2020-12-11Clarify changelog categories.Théo Zimmermann
For readers of the changelog: title "Tools" become "Command-line tools". For developers: changelog categories 07 and 08 are disambiguated.
2020-12-10Merge PR #13608: Changelog for 8.12.2.coqbot-app[bot]
Reviewed-by: jfehrle
2020-12-10Changelog for 8.12.2.Théo Zimmermann
2020-12-10Merge PR #12100: Fixing use of argument scopes in patterns + a further ↵coqbot-app[bot]
cleanup of constrintern.ml Reviewed-by: SkySkimmer Ack-by: ppedrot
2020-12-10Merge PR #13590: Move Azure jobs to GitHub Actions.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-10[ci] update url of autosubstEnrico Tassi
2020-12-10[ci] remove old overlays so that people don't copy themEnrico Tassi
2020-12-10[ci] simplify overlay scriptsEnrico Tassi
2020-12-10Move Azure jobs to GitHub Actions.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:31:49 +0000