1. 14 Sep, 2016 2 commits
  2. 09 Jun, 2016 1 commit
  3. 14 Mar, 2016 1 commit
  4. 01 Feb, 2016 1 commit
  5. 28 Jan, 2016 1 commit
  6. 26 Jan, 2016 2 commits
  7. 25 Jan, 2016 1 commit
  8. 25 Nov, 2015 2 commits
  9. 20 Nov, 2015 1 commit
  10. 19 Nov, 2015 1 commit
  11. 18 Nov, 2015 1 commit
  12. 13 Nov, 2015 1 commit
  13. 03 Nov, 2015 1 commit
  14. 19 Oct, 2015 1 commit
  15. 17 Oct, 2015 1 commit
  16. 16 Oct, 2015 1 commit
  17. 07 Oct, 2015 1 commit
    • Clément Fumex's avatar
      - some modifications to bv.why/mlw : · 8761602f
      Clément Fumex authored
        + size -> size_bv
        + size_int -> size
        + change two_power_size and max_int definitions
        + add axioms to BVConverter
        + new axiom relating nth and nth_bv
        + some reorganisation
      - update coq realisation
      - modify in consequence the relevant examples and pull the completed ones out of in_progress
      8761602f
  18. 28 Sep, 2015 1 commit
  19. 11 Sep, 2015 1 commit
  20. 01 Sep, 2015 1 commit
    • David Hauzar's avatar
      Projections of indices of maps. · baac0c6b
      David Hauzar authored
      The transformation intro_projections_counterexmp now can project maps
      with indices of types that should be projected (to type "t_to")
      to maps with indices that are projections of indices of original maps
      (they are of the type "t_to").
      baac0c6b
  21. 28 Aug, 2015 1 commit
  22. 20 Aug, 2015 2 commits
  23. 21 Jul, 2015 1 commit
  24. 20 Jul, 2015 1 commit
  25. 17 Jul, 2015 1 commit
  26. 16 Jul, 2015 1 commit
    • Martin Clochard's avatar
      discriminate: change way to configure the transformation · 336ea66d
      Martin Clochard authored
      This commit enable the possibility to change discriminate
      behavior from Why3 source files. The 4 metas that configure
      the transformation:
      
      select_inst
      select_lsinst
      select_lskept
      select_kept
      
      can now be configured from source files (actually they could
      before, but their value was overriden by the drivers).
      
      The behavior in absence of annotation can be specified from
      drivers using the 4 new configuration metas:
      
      select_inst_default
      select_lsinst_default
      select_lskept_default
      select_kept_default
      
      They behave as their non-default counterparts, except they
      have lower precedence. This avoid the forementioned
      overriding problem.
      336ea66d
  27. 10 Jul, 2015 3 commits
  28. 08 Jul, 2015 5 commits
  29. 07 Jul, 2015 1 commit
  30. 06 Jul, 2015 1 commit