aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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).
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to ↵Pierre-Marie Pédrot
be added Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
Reviewed-by: SkySkimmer Ack-by: gares
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Special commit to start benchmarking.Maxime Dénès
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
We fix it by reducing K-redexes the same in the both places (make_tuple and minimal_free_rels) which compute the dependencies of a dependent equality.
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
2020-08-20Modify Init/Specif.v to compile with -mangle-namesJasper Hugunin
2020-08-20Modify Init/Datatypes.v to compile with -mangle-names.Jasper Hugunin
All except `pair_equal_spec` completely addressed by moving dependent hypotheses before the colon.
2020-08-20Modify Init/Logic.v to compile with -mangle-names.Jasper Hugunin
This is related to coq/coq#6781. Most issues are with `destruct H` where H is the name of a binder in the goal; this is addressed by moving dependent assumptions before the colon. A different option would be adding `intros` tactics, but this repeats the names of hypotheses (in the type of the goal and in the proof script). Additionally, the `destruct H with (Q:=...)` form gets changed to `destruct (H ...)`, since the binder name `Q` is refreshed.
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-20Adding overlays.Pierre-Marie Pédrot
2020-08-20Do not store the transparent state in delayed dnets.Pierre-Marie Pédrot
We know statically that it is going to be the one provided at the time of lookup, so we simply fetch it from there.
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 13:50:07 +0000