aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
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-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-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-23Merge PR #12851: Extraction: At declaration point of a global, use its ↵Maxime Dénès
declaring name Reviewed-by: maximedenes
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-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
2020-08-19Improve `make approve-output`Jason Gross
It now silently does nothing rather than erroring with `mv: cannot stat 'output/*.out.real': No such file or directory` if there is no output to approve, and also correctly handles `output-coqtop` and `output-coqchk` rather than ignoring these directories. Fixes #12863
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
When calling an Ltac function, add specific locations when interpreting the function, when interpreting the arguments and when executating the call (in a TacArg).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:45:52 +0000