Skip to content
Snippets Groups Projects
New look: Off

Improving coding style

    • Closed Issue created by Ralf Jung @jung

    It would be a good idea to also enforce (via CI) the coding style improvements we have in Iris, here in the examples project:

    • no auto-generated names
    • import "options" file everywhere that sets Default Goal Selector
    • Enforce Local/Global via our coq-lint.sh

    Then we also should enable CI for MRs the same way we do for Iris.

    ✓ 3 of 3 checklist items completed · Edited
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items ...

    • Activity

    • Ralf Jung marked the checklist item no auto-generated names as completed

      marked the checklist item no auto-generated names as completed

    • Ralf Jung marked the checklist item import "options" file everywhere that sets Default Goal Selector as completed

      marked the checklist item import "options" file everywhere that sets Default Goal Selector as completed

    • Ralf Jung marked the checklist item Enforce Local/Global via our coq-lint.sh as completed

      marked the checklist item Enforce Local/Global via our coq-lint.sh as completed

    • Ralf Jung
      Ralf Jung @jung ·
      Author Owner

      Fixed by b3056546

    • Ralf Jung closed

      closed

    Please register or sign in to reply