1. 22 Mar, 2018 2 commits
  2. 13 Mar, 2018 1 commit
  3. 08 Mar, 2018 1 commit
  4. 06 Mar, 2018 2 commits
  5. 07 Feb, 2018 1 commit
  6. 06 Feb, 2018 1 commit
  7. 02 Feb, 2018 1 commit
  8. 01 Feb, 2018 2 commits
  9. 23 Jan, 2018 3 commits
  10. 21 Jan, 2018 1 commit
  11. 19 Jan, 2018 2 commits
  12. 18 Jan, 2018 4 commits
  13. 17 Jan, 2018 4 commits
  14. 11 Jan, 2018 1 commit
  15. 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
  16. 20 Dec, 2017 1 commit
    • Sylvain Dailler's avatar
      Cherry picked from a commit of Julien Thierry that aims at improving the · 4756c1cd
      Sylvain Dailler authored
      Coq printer.
      Also adding the "pretty-printed" generated realization.
      
      
      
      N604-045 Coq code easier to read
      
      * src/printer/coq.ml
      Added indentation in Why3's Coq printer using the OCaml Format pretty
      printing module.
      Changed the display of logic formulas and terms only.
      
      (cherry picked from commit 3453a65e0e5fca7e3aa16e22915ee3f079daf1c6)
      
      Conflicts:
      	src/printer/coq.ml
      	src/transform/gnat_split_conj.ml
      4756c1cd
  17. 11 Dec, 2017 6 commits
  18. 08 Dec, 2017 1 commit
  19. 05 Dec, 2017 1 commit
  20. 01 Dec, 2017 1 commit
  21. 30 Nov, 2017 1 commit
    • Sylvain Dailler's avatar
      Fixing bv theory after changes to theory bv.why. · 43657109
      Sylvain Dailler authored
      The former realization of bv used a bit of sign as the less significant
      bit which should be the most significant. It did not raise problems
      because to_int and to_uint were not linked by an axiom in the .why. Now,
      it is the case, so we rewrote function twos_complement and made some
      straightforward changes to the existing realization (surprisingly proofs
      are the same).
      43657109
  22. 01 Nov, 2017 1 commit
  23. 27 Oct, 2017 1 commit