{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":671522260,"defaultBranch":"master","name":"coq","ownerLogin":"rtetley","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2023-07-27T14:05:51.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/32383664?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1726841027.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"e1030a2c30469ed663f8e7e81613e7ac31649605","ref":"refs/heads/jump-to-def","pushedAt":"2024-09-20T14:03:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"wip provide location info for defined objects","shortMessageHtmlLink":"wip provide location info for defined objects"}},{"before":"846d97985c13e2d3df0bdcdf8477ca50590486ed","after":"686e63142c9eaceb7fed5247a42ef1137449c447","ref":"refs/heads/master","pushedAt":"2024-09-20T12:48:05.000Z","pushType":"push","commitsCount":548,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #19519: Uniformize semantics of :> in class after deprecation phase of #16230\n\nReviewed-by: SkySkimmer\nAck-by: jfehrle\nAck-by: Alizter\nCo-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2515789077\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19519\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19519/hovercard\" href=\"https://github.com/coq/coq/pull/19519\">coq#19519</a>: Uniformize semantics of :&gt; in class after depreca…"}},{"before":"38d6695084c9d38b5af7258a85702a1d01a49dce","after":"846d97985c13e2d3df0bdcdf8477ca50590486ed","ref":"refs/heads/master","pushedAt":"2024-06-26T08:13:02.000Z","pushType":"push","commitsCount":425,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #19276: Fix univ poly Scheme Equality with non stdlib univ mono f_equal\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2372536263\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19276\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19276/hovercard\" href=\"https://github.com/coq/coq/pull/19276\">coq#19276</a>: Fix univ poly Scheme Equality with non stdlib uni…"}},{"before":"9e106398694cb0139ba407a41cfbad9c8d7381f2","after":"38d6695084c9d38b5af7258a85702a1d01a49dce","ref":"refs/heads/master","pushedAt":"2024-05-17T07:42:18.000Z","pushType":"push","commitsCount":502,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #18970: Cleanup counter handling in newprofile\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2259096261\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18970\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18970/hovercard\" href=\"https://github.com/coq/coq/pull/18970\">coq#18970</a>: Cleanup counter handling in newprofile"}},{"before":"0f73c88282b408c44ed8ceb30f4a290373b668cb","after":"799824c4125e90e46c93bd374a2f7b920d4bb9f8","ref":"refs/heads/record_comments","pushedAt":"2024-04-03T10:53:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Add test for comment lexing and beautify","shortMessageHtmlLink":"Add test for comment lexing and beautify"}},{"before":"8564e805201e76853b01ecb56a8a3d62474dfe96","after":"0f73c88282b408c44ed8ceb30f4a290373b668cb","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T16:32:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Nicer beautify output\n\nFrom\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu\n.\n\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n    match c with\n    | Vert => Orange\n    | Orange => Rouge\n    | Rouge => Vert\n    end.\n\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\n  intro c0.\n  (** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\n  intro c0rou. (* /!\\   CRASH ON THIS LINE   /!\\ *)\n  (** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n  rewrite c0rou. cbn [coul_suiv]. reflexivity.\nQed.\n~~~\n\nproduce\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\nintro c0.\n(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\nintro c0rou.\n(* /!\\   CRASH ON THIS LINE   /!\\ *)\n(** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n(rewrite c0rou).\n(cbn[coul_suiv]).\nreflexivity.\nQed.\n~~~\n\ninstead of\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.Definition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.Theorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.Proof.intro c0.(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n       on suppose [c0 = Rouge]\n       et on doit alors prouver [coul_suiv c0 = Vert]\n       sous cette hypothèse supplémentaire ;\n       lorsque l'on introduit une hypothèse, on lui donne un nom. *)intro\n c0rou.(rewrite\n  (* /!\\   CRASH ON THIS LINE   /!\\ *)(** Le raisonnement sous-jacent est :\n        soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n        on peut s'en servir pour démontrer coul_suiv [c0 =\n        Vert]. *)c0rou).(cbn[coul_suiv]).reflexivity.Qed.\n~~~","shortMessageHtmlLink":"Nicer beautify output"}},{"before":"5ac06dca26bb7def8bb6d5ae3396d21d022c9353","after":"8564e805201e76853b01ecb56a8a3d62474dfe96","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T12:54:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Remove dubious between_commands use in comment lexing","shortMessageHtmlLink":"Remove dubious between_commands use in comment lexing"}},{"before":"f126ef0a933c545e2d33f3b7d709904364361cde","after":"5ac06dca26bb7def8bb6d5ae3396d21d022c9353","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T12:53:37.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Remove dubious between_commands use in comment lexing","shortMessageHtmlLink":"Remove dubious between_commands use in comment lexing"}},{"before":"8b3004d03900b42290845820ff54c5aae0ed4068","after":"f126ef0a933c545e2d33f3b7d709904364361cde","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T12:53:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Remove dubious between_commands use in comment lexing","shortMessageHtmlLink":"Remove dubious between_commands use in comment lexing"}},{"before":"4d99b9ea6c75d6cfaf6db3112b684169baea96df","after":"8b3004d03900b42290845820ff54c5aae0ed4068","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T12:09:51.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Nicer beautify output\n\nFrom\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu\n.\n\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n    match c with\n    | Vert => Orange\n    | Orange => Rouge\n    | Rouge => Vert\n    end.\n\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\n  intro c0.\n  (** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\n  intro c0rou. (* /!\\   CRASH ON THIS LINE   /!\\ *)\n  (** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n  rewrite c0rou. cbn [coul_suiv]. reflexivity.\nQed.\n~~~\n\nproduce\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\nintro c0.\n(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\nintro c0rou.\n(* /!\\   CRASH ON THIS LINE   /!\\ *)\n(** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n(rewrite c0rou).\n(cbn[coul_suiv]).\nreflexivity.\nQed.\n~~~\n\ninstead of\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.Definition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.Theorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.Proof.intro c0.(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n       on suppose [c0 = Rouge]\n       et on doit alors prouver [coul_suiv c0 = Vert]\n       sous cette hypothèse supplémentaire ;\n       lorsque l'on introduit une hypothèse, on lui donne un nom. *)intro\n c0rou.(rewrite\n  (* /!\\   CRASH ON THIS LINE   /!\\ *)(** Le raisonnement sous-jacent est :\n        soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n        on peut s'en servir pour démontrer coul_suiv [c0 =\n        Vert]. *)c0rou).(cbn[coul_suiv]).reflexivity.Qed.\n~~~","shortMessageHtmlLink":"Nicer beautify output"}},{"before":"7a10c9a40370a5ad3099582225758ded172b8509","after":"4d99b9ea6c75d6cfaf6db3112b684169baea96df","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T11:35:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Nicer beautify output\n\nFrom\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu\n.\n\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n    match c with\n    | Vert => Orange\n    | Orange => Rouge\n    | Rouge => Vert\n    end.\n\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\n  intro c0.\n  (** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\n  intro c0rou. (* /!\\   CRASH ON THIS LINE   /!\\ *)\n  (** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n  rewrite c0rou. cbn [coul_suiv]. reflexivity.\nQed.\n~~~\n\nproduce\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.\nDefinition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.\nTheorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.\nProof.\nintro c0.\n(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n      on suppose [c0 = Rouge]\n      et on doit alors prouver [coul_suiv c0 = Vert]\n      sous cette hypothèse supplémentaire ;\n      lorsque l'on introduit une hypothèse, on lui donne un nom. *)\nintro c0rou.\n(* /!\\   CRASH ON THIS LINE   /!\\ *)\n(** Le raisonnement sous-jacent est :\n      soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n      on peut s'en servir pour démontrer coul_suiv [c0 = Vert]. *)\n(rewrite c0rou).\n(cbn[coul_suiv]).\nreflexivity.\nQed.\n~~~\n\ninstead of\n\n~~~coq\nInductive coulfeu : Set :=\n  | Vert : coulfeu\n  | Orange : coulfeu\n  | Rouge : coulfeu.Definition coul_suiv : coulfeu -> coulfeu :=\n  fun c =>\n  match c with\n  | Vert => Orange\n  | Orange => Rouge\n  | Rouge => Vert\n  end.Theorem th_crou_gen : forall c : coulfeu, c = Rouge -> coul_suiv c = Vert.Proof.intro c0.(** Pour démontrer [c0 = Rouge -> coul_suiv c0 = Vert],\n       on suppose [c0 = Rouge]\n       et on doit alors prouver [coul_suiv c0 = Vert]\n       sous cette hypothèse supplémentaire ;\n       lorsque l'on introduit une hypothèse, on lui donne un nom. *)intro\n c0rou.(rewrite\n  (* /!\\   CRASH ON THIS LINE   /!\\ *)(** Le raisonnement sous-jacent est :\n        soit c0rou une preuve arbitraire (inconnue) de [c0 = Rouge],\n        on peut s'en servir pour démontrer coul_suiv [c0 =\n        Vert]. *)c0rou).(cbn[coul_suiv]).reflexivity.Qed.\n~~~","shortMessageHtmlLink":"Nicer beautify output"}},{"before":"848ecf1781d0a5d6a6e0b66e65d3dbe95b15b91e","after":"7a10c9a40370a5ad3099582225758ded172b8509","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T11:18:37.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Add debug flag for comment lexing","shortMessageHtmlLink":"Add debug flag for comment lexing"}},{"before":null,"after":"848ecf1781d0a5d6a6e0b66e65d3dbe95b15b91e","ref":"refs/heads/record_comments","pushedAt":"2024-03-19T09:16:16.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Create new record_comments flag","shortMessageHtmlLink":"Create new record_comments flag"}},{"before":"c3c67fa053313236aced3e987be21554d03c22c5","after":"9e106398694cb0139ba407a41cfbad9c8d7381f2","ref":"refs/heads/master","pushedAt":"2024-03-19T09:07:00.000Z","pushType":"push","commitsCount":224,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #18698: Declaremods collect_export: preserve strict equality\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2146770857\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18698\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18698/hovercard\" href=\"https://github.com/coq/coq/pull/18698\">coq#18698</a>: Declaremods collect_export: preserve strict equality"}},{"before":"432d113991703f7449eec340b4a4d1c36be4d77a","after":"90229ee3a6a65c9d088bc49b0e488a42f818b84f","ref":"refs/heads/loc-for-magic-version-check","pushedAt":"2024-02-22T13:54:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Waterfall the loc so that we record it in the magic number and version fail errors.\n\nThis enables locating the version and magic number check errors\nmore precisely.","shortMessageHtmlLink":"Waterfall the loc so that we record it in the magic number and versio…"}},{"before":"b13fcd9a79294d7c30642479738e55095a7acfcc","after":"e4efa55445c58c62397dc3cc0942a3a9f551456b","ref":"refs/heads/iraise-for-lib-errors","pushedAt":"2024-02-21T08:33:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Use Loc.raise instead of raise.\n\nThis has the benefit of forwarding the loc in a way that does not\nrequire special handling of the error case downstream.\nGives more precision to the location of the error on an IDE.","shortMessageHtmlLink":"Use Loc.raise instead of raise."}},{"before":"78d5b6ec9c2517b3c6644088ff192a9083dbaa58","after":"432d113991703f7449eec340b4a4d1c36be4d77a","ref":"refs/heads/loc-for-magic-version-check","pushedAt":"2024-02-20T17:04:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Code review","shortMessageHtmlLink":"Code review"}},{"before":"668b557761cc1432c8ad7106306f9c325ee134f2","after":"78d5b6ec9c2517b3c6644088ff192a9083dbaa58","ref":"refs/heads/loc-for-magic-version-check","pushedAt":"2024-02-20T17:03:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Corrected test suite","shortMessageHtmlLink":"Corrected test suite"}},{"before":"aa498e2850e51d870d2642301f4536c7f19d872a","after":"668b557761cc1432c8ad7106306f9c325ee134f2","ref":"refs/heads/loc-for-magic-version-check","pushedAt":"2024-02-20T15:35:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Modifications after code review. Update test suite.","shortMessageHtmlLink":"Modifications after code review. Update test suite."}},{"before":"dfd70f7567ffe7dfdf1988d4b8b891d3dab6c722","after":"b13fcd9a79294d7c30642479738e55095a7acfcc","ref":"refs/heads/iraise-for-lib-errors","pushedAt":"2024-02-20T15:18:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Update test suite","shortMessageHtmlLink":"Update test suite"}},{"before":null,"after":"aa498e2850e51d870d2642301f4536c7f19d872a","ref":"refs/heads/loc-for-magic-version-check","pushedAt":"2024-02-20T13:52:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Try to waterfall the loc so that we record it in the error.","shortMessageHtmlLink":"Try to waterfall the loc so that we record it in the error."}},{"before":"664f1e2138ea5d854e9ab6cd85ec50ee702ad07a","after":"dfd70f7567ffe7dfdf1988d4b8b891d3dab6c722","ref":"refs/heads/iraise-for-lib-errors","pushedAt":"2024-02-20T09:54:15.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Use Loc.raise instead of raise.\n\nThis has the benefit of forwarding a loc, which is then used by\nvscoq-language-server to correctly display the error message.","shortMessageHtmlLink":"Use Loc.raise instead of raise."}},{"before":null,"after":"664f1e2138ea5d854e9ab6cd85ec50ee702ad07a","ref":"refs/heads/iraise-for-lib-errors","pushedAt":"2024-02-19T15:32:00.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Use iraise instead of raise.\n\nThis has the benefit of forwarding a loc, which is then used by\nvscoq-language-server to correctly display the error message.","shortMessageHtmlLink":"Use iraise instead of raise."}},{"before":"0aad99ebdc75fc5d00a406bb9bd901dcc6bba5e0","after":"c3c67fa053313236aced3e987be21554d03c22c5","ref":"refs/heads/master","pushedAt":"2024-02-19T14:59:04.000Z","pushType":"push","commitsCount":43,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #18640: Revert \"Stop doing early universe minimization and nf_evar in abstract\"\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2125085728\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18640\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18640/hovercard\" href=\"https://github.com/coq/coq/pull/18640\">coq#18640</a>: Revert \"Stop doing early universe minimization an…"}},{"before":"c011e08a8ad1d075ba98ed54c7b008638117b02b","after":"0aad99ebdc75fc5d00a406bb9bd901dcc6bba5e0","ref":"refs/heads/master","pushedAt":"2024-02-15T14:06:00.000Z","pushType":"push","commitsCount":250,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #18675: Fix `unfold` tactic not unfolding compatibility constants.\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2132655323\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18675\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18675/hovercard\" href=\"https://github.com/coq/coq/pull/18675\">coq#18675</a>: Fix <code>unfold</code> tactic not unfolding compatibility c…"}},{"before":"84b707ef89d2308ffa07533791ffd47f1e66c4de","after":"544ab14e5618c34e60606c01d2a946f5d4a332c1","ref":"refs/heads/bump-vscoq","pushedAt":"2024-02-09T08:12:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"[ci] track vscoq on master","shortMessageHtmlLink":"[ci] track vscoq on master"}},{"before":"c253e81ca1a7132dd74445bf7bda3c0e35f1cfea","after":"84b707ef89d2308ffa07533791ffd47f1e66c4de","ref":"refs/heads/bump-vscoq","pushedAt":"2024-02-08T19:59:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"gares","name":"Enrico Tassi","path":"/gares","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1013846?s=80&v=4"},"commit":{"message":"Update .gitlab-ci.yml","shortMessageHtmlLink":"Update .gitlab-ci.yml"}},{"before":"091a34af875062a078c203daac36072d6b1e20e6","after":"c253e81ca1a7132dd74445bf7bda3c0e35f1cfea","ref":"refs/heads/bump-vscoq","pushedAt":"2024-02-08T19:54:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"gares","name":"Enrico Tassi","path":"/gares","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1013846?s=80&v=4"},"commit":{"message":"Update .gitlab-ci.yml","shortMessageHtmlLink":"Update .gitlab-ci.yml"}},{"before":null,"after":"091a34af875062a078c203daac36072d6b1e20e6","ref":"refs/heads/bump-vscoq","pushedAt":"2024-02-08T15:34:30.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Dropped overlay","shortMessageHtmlLink":"Dropped overlay"}},{"before":"b7c08147339b2d26da4fb39e68be2124b4a56489","after":"c011e08a8ad1d075ba98ed54c7b008638117b02b","ref":"refs/heads/master","pushedAt":"2024-01-30T14:46:48.000Z","pushType":"push","commitsCount":619,"pusher":{"login":"rtetley","name":"Romain Tetley","path":"/rtetley","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32383664?s=80&v=4"},"commit":{"message":"Merge PR #18498: doc NZBase, NZadd, NZOrder\n\nReviewed-by: proux01\nCo-authored-by: proux01 <proux01@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2082474981\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18498\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18498/hovercard\" href=\"https://github.com/coq/coq/pull/18498\">coq#18498</a>: doc NZBase, NZadd, NZOrder"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yMFQxNDowMzo0Ny4wMDAwMDBazwAAAAS8CIAa","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMS0zMFQxNDo0Njo0OC4wMDAwMDBazwAAAAPtDdI0"}},"title":"Activity · rtetley/coq"}