1. 24 Mar, 2021 1 commit
  2. 23 Mar, 2021 2 commits
  3. 16 Mar, 2021 4 commits
    • Michael Sammler's avatar
      update queue with version from master · 7e5afceb
      Michael Sammler authored
      7e5afceb
    • Michael Sammler's avatar
      update data generation script · 4e538af3
      Michael Sammler authored
      4e538af3
    • Michael Sammler's avatar
      update code of example · 0c5bc27d
      Michael Sammler authored
      0c5bc27d
    • Rodolphe Lepigre's avatar
      Make RefinedC more user-friendly with several changes. · 3cefc49b
      Rodolphe Lepigre authored and Michael Sammler's avatar Michael Sammler committed
      The first change concern the syntax of constraints in annotations. The following is now allowed:
      - [own l : ty] (previously written [l @ &own<ty>]),
      - [shr l : ty] (previously written [l @ &shr<ty>]),
      - [frac β l : ty] (previously written [l @ &frac<β, ty>]).
      - The old notations have been removed.
      
      The second change is some renaming around singleton types and layouts:
      - [singleton_val] is now called [value],
      - [singleton_place] is now called [place],
      - [LPtr] is now called [void_ptr] and is accessed with notation [void*],
      - [LVoid] is now called [void_layout].
      - The front end now accepts `void*` as an identifier.
      
      The last change introduces a new Coq scope called [printing_sugar] that is only opened at the beginning of proofs in generated proof files. It defines printing notations intended at making the output of the tool closer to the syntax of the front end. In particular it defines the following notations:
      - [own l : ty], [shr l : ty], [frac {β} l : ty],
      - [uninit<ly>], [value<ly, v>], [place<l>], [&own<ty>], ...
      - For each user-defined types a similar printing sugar is defined automatically.
      3cefc49b
  4. 02 Mar, 2021 1 commit
  5. 01 Mar, 2021 2 commits
  6. 18 Nov, 2020 6 commits
  7. 17 Nov, 2020 2 commits
  8. 16 Nov, 2020 2 commits
  9. 13 Nov, 2020 1 commit
  10. 12 Nov, 2020 1 commit
  11. 11 Nov, 2020 2 commits
  12. 10 Nov, 2020 5 commits
  13. 09 Nov, 2020 1 commit
  14. 05 Nov, 2020 1 commit
  15. 04 Nov, 2020 1 commit
  16. 03 Nov, 2020 1 commit
  17. 02 Nov, 2020 1 commit
  18. 29 Oct, 2020 3 commits
  19. 22 Oct, 2020 1 commit
  20. 21 Oct, 2020 2 commits
    • Rodolphe Lepigre's avatar
      Renaming [block_id] into [label]. · c0ffc3f9
      Rodolphe Lepigre authored
      Using [block_id] to refer to the first component of locations.
      c0ffc3f9
    • Rodolphe Lepigre's avatar
      Refactoring and renaming in [lang.v] (mostly). · 5552a911
      Rodolphe Lepigre authored
      - Put stuff in sections in [lang.v].
      - Renamed [mk_layout] into [Layout] (for uniformity).
      - Renamed [it_min] and [it_max] into [max_int] and [min_int].
      - Some other renamings on [int_type]-related stuff.
      - Changed [max_int] to be the last representable integer.
      - Turned [in_it_range] into an instance of [ElemOf].
      5552a911