aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
2020-12-21Remove the artificial dependency of Heads on evaluable_global_reference.Pierre-Marie Pédrot
2020-12-20Merge PR #13138: Towards a documentation / cleanup of evarconvcoqbot-app[bot]
Reviewed-by: gares
2020-12-18Merge PR #13530: Revert removal of eoi_entry in #13447coqbot-app[bot]
Reviewed-by: herbelin
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: gares Ack-by: SkySkimmer
2020-12-17Merge PR #13652: Add a test for change over case nodes.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
This is extracted from #13563.
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
This will help with reproducibility for people who have something in their coqrc file. Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-16Merge PR #13644: Fix overlay system: projects need to be loaded before overlays.coqbot-app[bot]
Reviewed-by: gares
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-16Merge PR #13616: Bench: add .log extension to .stdout/stderr filesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
Also fixes is_in_projects
2020-12-15Merge PR #13615: Document the manual tasks that I need to do at each release.coqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13625: Tweak constr_matching so as to make it tail-rec on ↵coqbot-app[bot]
projection expansion. Reviewed-by: ejgallego
2020-12-15Merge PR #13633: [ci] uniform name of projects w.r.t. opam packagescoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
Reviewed-by: herbelin
2020-12-15Merge PR #13621: Fast path in tclPROGRESS.coqbot-app[bot]
Reviewed-by: herbelin
2020-12-15Merge PR #13632: [ci] Update pin ci scriptcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-15[ci] uniform name of projects w.r.t. opam packagesEnrico Tassi
This makes it easier to track projects across Coq's CI and the platform
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-14Merge PR #13630: Cleanup reductionopscoqbot-app[bot]
Reviewed-by: gares
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:21:08 +0000