aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-25Modify Classes/CRelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/Morphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
The apply <- tactic was breaking, so we had to modify the definition in Init/Tactics.v to use slightly fresher names.
2020-08-25Modify Bool/Bool.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Tactics.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Wf.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Peano.v to compile with -mangle-names.Jasper Hugunin
Here I added intros rather than moving premises before the colon, partly to be more consistent with nearby lemma statements.
2020-08-25Merge PR #12879: added numeral_notation to META.coq.incoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: Alizter Ack-by: gares
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
Reviewed-by: Zimmi48
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-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-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-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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:47:27 +0000