1. 06 Feb, 2018 1 commit
  2. 11 Jan, 2018 1 commit
  3. 24 Dec, 2017 1 commit
    • Guillaume Melquiond's avatar
      Create directories bin and lib/plugins on the fly (bug #21566). · 3698ec54
      Guillaume Melquiond authored
      Some people dump the content of tarballs into git repositories and thus
      experience compilation failures. Indeed, some directories from the tarball
      are empty and thus not preserved by git. So this commit creates these
      directories on the fly.
      
      As for plugins/printer, it has to be handled differently, since it is
      needed by ocamldep and thus cannot be created on the fly. So its .keepme
      file is put in the tarball to keep it nonempty.
      3698ec54
  4. 11 Dec, 2017 6 commits
  5. 08 Dec, 2017 1 commit
  6. 01 Nov, 2017 1 commit
  7. 03 Oct, 2017 1 commit
  8. 30 Sep, 2017 1 commit
  9. 27 Sep, 2017 1 commit
  10. 26 Sep, 2017 1 commit
  11. 08 Sep, 2017 1 commit
  12. 12 Apr, 2017 1 commit
  13. 11 Apr, 2017 4 commits
  14. 10 Apr, 2017 1 commit
  15. 17 Mar, 2017 1 commit
  16. 07 Mar, 2017 1 commit
    • Clément Fumex's avatar
      + use literals in ieee_float theory · f88de190
      Clément Fumex authored
      + add 'minInt and 'maxInt attributes for range types
      + add 'eb and 'sb attributes for float types
      + make ieee_float realization compatible with Coq 8.4
      f88de190
  17. 28 Feb, 2017 2 commits
    • Clément Fumex's avatar
      Add the ability to · f0547868
      Clément Fumex authored
      * declare range types and float types,
      * use integer (resp. real) literals for those types through casting,
      * specify how to print them in drivers.
      
      Change in syntax
      * use
      
        type t = < range 1 2 >   (* integers from 1 to 2 *)
        type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
      
        the two projections :
        t'int
        t''real
      
        and the predicate :
        t''isFinite
      
      * Restrict the use of "'" in whyml:
        Users are not allowed to introduce names where a quote symbol
        is followed by a letter. Thus, the following identifiers are
        valid:
      
        t'
        toto'0''
        toto'_phi
      
        whereas toto'phi is not.
      
      Note: we do not yet support negative numbers in range declaration
      and casting of a literal.
      f0547868
    • Guillaume Melquiond's avatar
      Generalize negative_or_positive. · 788027d2
      Guillaume Melquiond authored
      788027d2
  18. 27 Feb, 2017 1 commit
  19. 25 Jan, 2017 1 commit
    • Clément Fumex's avatar
      + remove unused constant half · 5a44ec01
      Clément Fumex authored
      + add predicate "exact_int"
      + add three axioms on of_int +/-/*
      + add some other axioms
      + guard the theory realization with a dependency to flocq in make file
      5a44ec01
  20. 05 Jan, 2017 2 commits
  21. 03 Jan, 2017 3 commits
  22. 19 Oct, 2016 1 commit
  23. 05 Jul, 2016 1 commit
  24. 30 Jun, 2016 1 commit
  25. 09 May, 2016 1 commit
  26. 15 Mar, 2016 2 commits
  27. 24 Feb, 2016 1 commit