{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":571145487,"defaultBranch":"master","name":"coq","ownerLogin":"Villetaneuse","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2022-11-27T10:14:23.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/119015057?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1720102150.0","currentOid":""},"activityList":{"items":[{"before":"c1b6cf4ecff5bc8916723fb84c7d49744a0e82ad","after":"9dfe019abada404fe6a208fc0fdeabde4718584f","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-06T10:11:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Make introductory paragraphs clearer in summaries\n\nTake into account @jfehrle's remarks.","shortMessageHtmlLink":"Make introductory paragraphs clearer in summaries"}},{"before":"db561e85039844629d00cda987c67cd0997def8b","after":"c1b6cf4ecff5bc8916723fb84c7d49744a0e82ad","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-06T08:54:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Clarify locality rules for some commands in refman\n\nHere are the modified entries:\n- Definition\n- Axiom\n- Notation (abbreviation)\n- Canonical Structure\n- Set","shortMessageHtmlLink":"Clarify locality rules for some commands in refman"}},{"before":"e287e4181dcd4d78df198beabe9a725e74550624","after":"db561e85039844629d00cda987c67cd0997def8b","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-06T07:03:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"correct output for section table","shortMessageHtmlLink":"correct output for section table"}},{"before":"20a01ed43c290c129eaa3bfc33838c623fe5c674","after":"e287e4181dcd4d78df198beabe9a725e74550624","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-05T09:13:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add links to refman in test files\n\nThe goal is to ease maintenance if one of the test files fails following\na change in some command behaviour regarding locality.","shortMessageHtmlLink":"Add links to refman in test files"}},{"before":"6aafccc49df2b1db428f8c609c8864a7c778db8f","after":"20a01ed43c290c129eaa3bfc33838c623fe5c674","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-04T10:43:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add links to refman in test files\n\nThe goal is to ease maintenance if one of the test files fails following\na change in some command behaviour regarding locality.","shortMessageHtmlLink":"Add links to refman in test files"}},{"before":"9097c065aea482d81ef47f435640d6fb1e6875df","after":"6aafccc49df2b1db428f8c609c8864a7c778db8f","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-04T10:28:04.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add visibility rules in section in module\n\nA local definition in a section is also local in the current module.\nAn export/global setting in a section is also export/global in the\ncurrent module. Unfortunately, this makes the section table more\ncomplicated.\n\nThe section part of the refman is also slightly modified:\n- a subtitle \"Using sections\" appears before the description of the\n  commands, in order to have a better TOC\n- In the first sentences, \"declarations\" was inaccurate, since Let\n  introduces definitions\n- The \"Note\" starting with \"Most commands\" refers to the locality table","shortMessageHtmlLink":"Add visibility rules in section in module"}},{"before":"9e34f9506bd12ffecdb4c97ab7e23c6a4d4857d0","after":"9097c065aea482d81ef47f435640d6fb1e6875df","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-04T10:04:44.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add visibility rules in section in module\n\nA local definition in a section is also local in the current module.\nAn export/global setting in a section is also export/global in the\ncurrent module. Unfortunately, this makes the section table more\ncomplicated.\n\nThe section part of the refman is also slightly modified:\n- a subtitle \"Using sections\" appears before the description of the\n  commands, in order to have a better TOC\n- In the first sentences, \"declarations\" was inaccurate, since Let\n  introduces definitions\n- The \"Note\" starting with \"Most commands\" refers to the locality table","shortMessageHtmlLink":"Add visibility rules in section in module"}},{"before":"1b6c10becf30122b6cdfa160e1d9cde61017e26b","after":"9e34f9506bd12ffecdb4c97ab7e23c6a4d4857d0","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-03T16:23:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add visibility rules in section in module\n\nA local definition in a section is also local in the current module.\nAn export/global setting in a section is also export/global in the\ncurrent module.","shortMessageHtmlLink":"Add visibility rules in section in module"}},{"before":"8c63bb6d5cca27dcc333f6bc9da95a57d446ff7a","after":"1b6c10becf30122b6cdfa160e1d9cde61017e26b","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-03T16:13:15.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add test file about visib in section in module\n\nWe needed to test when locality attributes in a section in a module\naffect the visibility outside the module.","shortMessageHtmlLink":"Add test file about visib in section in module"}},{"before":"a30563f8805d148d77d576ef827cf0203f153c4f","after":"8c63bb6d5cca27dcc333f6bc9da95a57d446ff7a","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-03T15:38:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add test file about visib in section in module\n\nWe needed to test when locality attributes in a section in a module\naffect the visibility outside the module.","shortMessageHtmlLink":"Add test file about visib in section in module"}},{"before":"a0ab90534829e6e3ce80654c5b569b16b1fa4ae0","after":"a30563f8805d148d77d576ef827cf0203f153c4f","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-08-02T07:39:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Clarify meaning of entries in tables\n\nAlso group commands by similar behaviour.","shortMessageHtmlLink":"Clarify meaning of entries in tables"}},{"before":"ddec6575162c52a6572e43fdc8e4a544f3a628f4","after":"a0ab90534829e6e3ce80654c5b569b16b1fa4ae0","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-09T10:25:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"try to shorten modules table","shortMessageHtmlLink":"try to shorten modules table"}},{"before":"a7557824d4c68e9cc85094cca3367509a9c73ce8","after":"ddec6575162c52a6572e43fdc8e4a544f3a628f4","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-09T10:22:02.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Move \"Typing modules\" to the end","shortMessageHtmlLink":"Move \"Typing modules\" to the end"}},{"before":"c1866d1c12fbcf63304792ae8c33fadb49aa3589","after":"a7557824d4c68e9cc85094cca3367509a9c73ce8","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-09T09:45:48.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Move \"Typing modules\" to the end","shortMessageHtmlLink":"Move \"Typing modules\" to the end"}},{"before":"7c838f1175eec7621282045cc4144e15cabd9273","after":"c1866d1c12fbcf63304792ae8c33fadb49aa3589","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-06T13:16:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Update doc/sphinx/language/core/sections.rst\n\nCo-authored-by: Jim Fehrle <jim.fehrle@gmail.com>","shortMessageHtmlLink":"Update doc/sphinx/language/core/sections.rst"}},{"before":"4aabfc1e62ab9c84a61553f811383e5b784ad2c0","after":"7c838f1175eec7621282045cc4144e15cabd9273","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-05T16:16:59.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"clarify first sentence before tables","shortMessageHtmlLink":"clarify first sentence before tables"}},{"before":"3fd36d0d9d32dee16d77118f7672e856a0dda224","after":"4aabfc1e62ab9c84a61553f811383e5b784ad2c0","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-05T15:48:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"clarify first sentence before tables","shortMessageHtmlLink":"clarify first sentence before tables"}},{"before":"c7c4fd9aadba9450ebfdc86343a291bcc7236ff8","after":"3fd36d0d9d32dee16d77118f7672e856a0dda224","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-05T15:45:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"add test files locality/ltac2","shortMessageHtmlLink":"add test files locality/ltac2"}},{"before":"00fd874c3f5f4f94327a8caf25113f2c0736294e","after":"c7c4fd9aadba9450ebfdc86343a291bcc7236ff8","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-05T15:34:52.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"add test files except for Ltac2","shortMessageHtmlLink":"add test files except for Ltac2"}},{"before":"30a28e4d6f619610ea8f29c7055cc2bfc8a5f640","after":"00fd874c3f5f4f94327a8caf25113f2c0736294e","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-05T09:05:18.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add locality rules for sections","shortMessageHtmlLink":"Add locality rules for sections"}},{"before":"062067f8878b82d44ddcb5269bb4b4588262397f","after":"30a28e4d6f619610ea8f29c7055cc2bfc8a5f640","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T16:25:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Add locality rules for sections","shortMessageHtmlLink":"Add locality rules for sections"}},{"before":"5eddea0d09de22b89cba1a449aa2c987729cdc8f","after":"062067f8878b82d44ddcb5269bb4b4588262397f","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T16:12:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Hint is not a command","shortMessageHtmlLink":"Hint is not a command"}},{"before":"3b7fb67adb8de1f63d7a6cd3ffb61e57c705043a","after":"5eddea0d09de22b89cba1a449aa2c987729cdc8f","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T14:33:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"typo and Cmd","shortMessageHtmlLink":"typo and Cmd"}},{"before":"5b0a29d94deba3cecda816ab9a302c65e99f8b8a","after":"3b7fb67adb8de1f63d7a6cd3ffb61e57c705043a","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T14:29:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Update doc/sphinx/language/core/modules.rst\n\nCo-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>","shortMessageHtmlLink":"Update doc/sphinx/language/core/modules.rst"}},{"before":"2f6814ef36c1c927e138b1fa92033062032bb932","after":"5b0a29d94deba3cecda816ab9a302c65e99f8b8a","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T14:28:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Update doc/sphinx/language/core/modules.rst\n\nCo-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>","shortMessageHtmlLink":"Update doc/sphinx/language/core/modules.rst"}},{"before":"bc4f1755e89278b84e1843c22f955a63d726d3c5","after":"2f6814ef36c1c927e138b1fa92033062032bb932","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T14:28:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Update doc/sphinx/language/core/modules.rst\n\nCo-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>","shortMessageHtmlLink":"Update doc/sphinx/language/core/modules.rst"}},{"before":null,"after":"bc4f1755e89278b84e1843c22f955a63d726d3c5","ref":"refs/heads/add_locality_table_modules","pushedAt":"2024-07-04T14:09:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"add table of locality attributes in refman","shortMessageHtmlLink":"add table of locality attributes in refman"}},{"before":"838648f66d024db972316c48e2d9b8de030367f4","after":"ac79ea4cc6223dd5dd4d5efd04fcfcfd308f59f6","ref":"refs/heads/Include_module_type_with_definition","pushedAt":"2024-06-08T07:42:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"add changelog\n\nCo-authored-by: Jim Fehrle <jim.fehrle@gmail.com>","shortMessageHtmlLink":"add changelog"}},{"before":"1e77b3d02fb7d4a41f99baa8227bb55393228b2d","after":"838648f66d024db972316c48e2d9b8de030367f4","ref":"refs/heads/Include_module_type_with_definition","pushedAt":"2024-06-04T13:32:16.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"add changelog\n\nCo-authored-by: Jim Fehrle <jim.fehrle@gmail.com>","shortMessageHtmlLink":"add changelog"}},{"before":null,"after":"1e77b3d02fb7d4a41f99baa8227bb55393228b2d","ref":"refs/heads/Include_module_type_with_definition","pushedAt":"2024-06-04T13:25:56.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Villetaneuse","name":"Pierre Rousselin","path":"/Villetaneuse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119015057?s=80&v=4"},"commit":{"message":"Update doc/changelog/08-vernac-commands-and-options/18482-remove-include-type.rst\n\nCo-authored-by: Jim Fehrle <jim.fehrle@gmail.com>","shortMessageHtmlLink":"Update doc/changelog/08-vernac-commands-and-options/18482-remove-incl…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0wNlQxMDoxMToxMi4wMDAwMDBazwAAAASS8bTv","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0wNlQxMDoxMToxMi4wMDAwMDBazwAAAASS8bTv","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0wNFQxMzoyNTo1Ni4wMDAwMDBazwAAAARcD8VW"}},"title":"Activity · Villetaneuse/coq"}