aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-25Deprecate intro_usingGaëtan Gilbert
This is a footgun as it can refresh the name. Callers can still ignore the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
2020-08-25omega: stop using intro_usingGaëtan Gilbert
This makes the test suite Omega.v compatible with Mangle Names Not sure how `reintroduce` works since it ignores the refreshed name, considering omega is deprecated it's not worth figuring out so long as it works (NB making it use intro_mustbe_force makes the test suite fail so it must be doing something right).
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25elim.ml: stop using intro_usingGaëtan Gilbert
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
Fix #12676
2020-08-25fix notation-incompatible-format warningsReynald Affeldt
(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
Fix #12889
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25added coq.vernac dependency to string_notations pluginAli Caglayan
2020-08-25Merge PR #12888: Add /dev/bench to CODEOWNERScoqbot-app[bot]
Reviewed-by: Zimmi48
2020-08-25Merge PR #12728: Fix slow Print Universes Subgraph when many ambient universes.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Dead code in adjust_implicit_arguments.Hugo Herbelin
2020-08-25added coq.vernac dependency to numeral_notations pluginAli Caglayan
2020-08-25Merge PR #12882: Perform a few tweaks to make the bench script work properly.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ppedrot
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Merge PR #12870: CI: stop testing 4.11+trunkcoqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Merge PR #12778: Merging is now possible with coqbot.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Fix slow Print Universes Subgraph when many ambient universes.Gaëtan Gilbert
Fix #12688. Original test: ~~~coq Record my_mod: Type := mk { datatype: Type; }. Print Universes Subgraph (my_mod.u0). (* OK *) From ITree Require Export ITree. (* using coq-itree for the sake of example *) Print Universes Subgraph (my_mod.u0). (* Runs forever (> 1 min) *) ~~~ The issue is that we produce a subgraph with the user-given universes + Set and Prop. In the test the user given universes are not connected to other universes, but Set is below every universe so we traverse the whole graph. We can go faster by just checking whether Set is strictly below each universe we're interested in. Maybe this would be better handled at the ugraph level but that requires thinking about lbound so I didn't do it. I tested locally with Require Reals, which makes the print take about 0.1s on my PC before this patch. This is enough to check that we're now faster (near-instant) but not enough for automatic testing. Note that the other uses of UGraph.constraints_for (for private polymorphic universes and for context restriction) are interested in all ambient universes so the traversals starting at Set end quickly and do not cause the same issue.
2020-08-25add contra lemmas introduced by MathComp's PR #499Reynald Affeldt
(https://github.com/math-comp/math-comp/pull/499/)
2020-08-25tentative backport of ssrbool from MathComp 1.11Reynald Affeldt
2020-08-25Merge PR #12878: Update sigma instead of erasing it in `update_global_env`coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25Add /dev/bench to CODEOWNERSGaëtan Gilbert
2020-08-24Merge PR #12886: Fix Coqtail test directory.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-08-24Fix Coqtail test directory.whonore
Tests moved in https://github.com/whonore/Coqtail/pull/134.
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-24Merge PR #12868: Lint stdlib with -mangle-names #1Anton Trunov
Reviewed-by: anton-trunov
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its ↵Hugo Herbelin
documentation Reviewed-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: jfehrle
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵coqbot
recognition. Reviewed-by: mattam82
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-24Bench: artifact logsGaëtan Gilbert
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
Reviewed-by: mattam82 Ack-by: ppedrot
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ↵coqbot
exist Reviewed-by: SkySkimmer
2020-08-24Merge PR #12832: Introduce GitHub Action to check for conflicts in PRs.coqbot
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence ↵Pierre-Marie Pédrot
of artificial dependencies disappearing by reduction Reviewed-by: ppedrot
2020-08-24CI: stop testing 4.11+trunkGaëtan Gilbert
Now that 4.11.0 is released the trunk job doesn't work. 4.12 also doesn't work for separate reasons ("No rule found for kernel/byterun/byterun.a") We will separately update the edge switch in the docker image to use 4.11.0.
2020-08-24added numeral_notation to META.coq.inAli Caglayan
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its ↵Maxime Dénès
declaring name Reviewed-by: maximedenes
2020-08-22Namegen.visible_ids: fixing what seems to be typos.Hugo Herbelin
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-21Use a map function instead of a fold when freezing summaries.Pierre-Marie Pédrot
This is O(n) instead of O(n log n) and should be more efficient in practice.
2020-08-21Add a heterogeneous map function over Dyn.Map.Pierre-Marie Pédrot
2020-08-21Add Actions to CI realm in CODEOWNERS.Théo Zimmermann
2020-08-21Introduce GitHub Action to check for conflicts in PRs.Théo Zimmermann
Alternative to adding this feature to coqbot (coq/bot#14).
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-03 00:06:35 +0000