1. 30 May, 2022 4 commits
    • Samuel Hym's avatar
      Bump version · 0a6c5510
      Samuel Hym authored
      0a6c5510
    • Samuel Hym's avatar
      Update copyright notices · 0f6f0949
      Samuel Hym authored
      0f6f0949
    • Samuel Hym's avatar
      CI: Use local debian mirror instead of cache. · 6df6e01c
      Samuel Hym authored
      Use the local debian mirror instead of the global one
      Only install the required packages, not all the recommended ones
      Use a short expiring date for artifacts, in cases of quick succession of
      CI builds, only the most recent is to be kept
      6df6e01c
    • Samuel Hym's avatar
      Collect types also for non-monadic functions · 1b4513eb
      Samuel Hym authored
      Primitive operations in C world, such as `==`, `&&`, etc. are naturally
      represented as non-monadic functions in Gallina.
      
      With this patch, given this code:
      
          do x <- returnM (eqb y z) ;
          ...
      
      the type for x is properly generated as the return type of eqb, without
      requiring an explicit definition of a monadic lifting of eqb.
      1b4513eb
  2. 27 Apr, 2022 1 commit
  3. 14 Apr, 2022 1 commit
  4. 10 Feb, 2021 1 commit
  5. 09 Feb, 2021 1 commit
  6. 05 Feb, 2021 1 commit
  7. 10 Nov, 2020 2 commits
  8. 05 Nov, 2020 2 commits
  9. 16 Dec, 2019 2 commits
  10. 24 Apr, 2019 1 commit
  11. 12 Apr, 2019 5 commits
  12. 02 Nov, 2018 1 commit
  13. 17 Oct, 2018 2 commits
  14. 29 Sep, 2017 2 commits
  15. 04 Aug, 2017 1 commit
    • Samuel Hym's avatar
      Rewrite coq2c. Rename it digger. · d24f5e53
      Samuel Hym authored
      Refactor the code parsing the JSON extracted from Coq.
      
      Rewrite completely the conversion to C, splitting it in two stages:
      - from the Coq AST to an intermediate representation corresponding to
        the part of Gallina that we can map to C,
      - from that intermediate representation to C.
      
      Use the standard Language.C library to produce the resulting C code, to
      strengthen its quality.
      d24f5e53
  16. 03 Oct, 2016 5 commits