Commits · 6a0302bc53fe5d60858099b30d1a0679fa7eb76c · Why3 / why3

07 Nov, 2017 1 commit
- update session · 6a0302bc
  Raphael Rieu-Helft authored Nov 07, 2017
  
  6a0302bc
06 Nov, 2017 1 commit
- Add reification check · b2201ded
  Raphael Rieu-Helft authored Nov 06, 2017
  
  b2201ded
03 Nov, 2017 1 commit
- preuve de strassen par réflexion · f3b04e9c
  Raphael Rieu-Helft authored Nov 03, 2017
  
  f3b04e9c
31 Oct, 2017 2 commits
- Infinite matrices definitions · ab3922d4
  Raphael Rieu-Helft authored Oct 31, 2017
  
  ab3922d4
- reification and normalization transformations · df04199d
  Raphael Rieu-Helft authored Oct 31, 2017
  
  df04199d
24 Oct, 2017 1 commit
- add reification transformation (wip) · 7c2ead74
  Raphael Rieu-Helft authored Oct 24, 2017
  
  7c2ead74
12 Oct, 2017 1 commit
- Merge branch 'new_system' into mp · 96afb1a7
  Raphael Rieu-Helft authored Oct 12, 2017
  
  96afb1a7
11 Oct, 2017 2 commits
- example 2wp_gen(in progress): added conversions games/transition systems. · e8fd72b7
  Martin Clochard authored Oct 11, 2017
  
  e8fd72b7
- Coercion in mach.onetime.OneTime using the type field · b0bfbb0b
  Mário Pereira authored Oct 11, 2017
  
  b0bfbb0b
10 Oct, 2017 2 commits
- OCaml64: added constant one from mach.peano.Peano · 26b2b97c
  Mário Pereira authored Oct 10, 2017
  
  26b2b97c
- Extraction: nicer printing of functors modules · bea2bd78
  Mário Pereira authored Oct 10, 2017
  
  bea2bd78
09 Oct, 2017 1 commit
- Decision procedure on algebras · d4fbc21f
  Raphael Rieu-Helft authored Oct 09, 2017
  
  d4fbc21f
06 Oct, 2017 1 commit
- Generalize decision procedure to commutative rings · 06da7413
  Raphael Rieu-Helft authored Oct 06, 2017
  
  06da7413
05 Oct, 2017 1 commit
- Finish reflection example · ccd627af
  Raphael Rieu-Helft authored Oct 05, 2017
  
  ccd627af
04 Oct, 2017 1 commit
- Reflection toy example · 7fc10633
  Raphael Rieu-Helft authored Oct 04, 2017
  
  7fc10633
03 Oct, 2017 2 commits
- Merge branch 'master' into new_system · d754ddee
  Guillaume Melquiond authored Oct 03, 2017
  
  d754ddee
- Fix compilation with Coq 8.4 and 8.5, and remove tactic support for 8.4. · 903d9f69
  Guillaume Melquiond authored Oct 03, 2017
  
  903d9f69
02 Oct, 2017 4 commits
- Remove unused pictures. · 99bcc7e3
  Guillaume Melquiond authored Oct 02, 2017
  
  99bcc7e3
- fix proof · d7cf96b1
  Raphael Rieu-Helft authored Oct 02, 2017
  
  d7cf96b1
- Merge branch 'new_system' into mp · f919ac7c
  Raphael Rieu-Helft authored Oct 02, 2017
```
Conflicts:
	src/mlw/compile.ml
	src/mlw/ocaml_printer.ml
	src/tools/why3extract.ml
```
  f919ac7c
- Give proper names to documentation html files. · 28e12b62
  Guillaume Melquiond authored Oct 02, 2017
  
  28e12b62
30 Sep, 2017 1 commit
- Partly realize some missing theories of ieee_float. · 153df9d2
  Guillaume Melquiond authored Sep 30, 2017
  
  153df9d2
29 Sep, 2017 3 commits
- Do no longer play tricks with headers of Coq realizations. · 88236a24
  Guillaume Melquiond authored May 24, 2017
  
  88236a24
- Preserve realization headers in Coq printer. · eeeb58d9
  Guillaume Melquiond authored May 24, 2017
  
  eeeb58d9
- Remove some unused code. · aafbd002
  Guillaume Melquiond authored Sep 28, 2017
  
  aafbd002
28 Sep, 2017 4 commits
- updated drivers with eliminate_literal · a6d89023
  MARCHE Claude authored Sep 28, 2017
  
  a6d89023
- fill the file CHANGES plus minor changes in the manual · 02acc89f
  MARCHE Claude authored Sep 28, 2017
  
  02acc89f
- adding strategy auto 0, same as level 1 but without split · 785df505
  MARCHE Claude authored Sep 21, 2017
  
  785df505
- Support for Isabelle 2017 · 5878d5a1
  MARCHE Claude authored Sep 28, 2017
```
Merges remote-tracking branch 'berghofer/master'
```
  5878d5a1
27 Sep, 2017 2 commits
- adjust for supporting both Coq 8.5 and Coq 8.6 · 7c7797db
  MARCHE Claude authored Sep 27, 2017
  
  7c7797db
- Added ocp-indent configuration file · 4b3854a2
  Mário Pereira authored Sep 27, 2017
  
  4b3854a2
26 Sep, 2017 5 commits
- Remove unused code. · e07b4d55
  Guillaume Melquiond authored Sep 26, 2017
  
  e07b4d55
- Remove configure check for -bin-annot since OCaml 4.02.3 is required. · 5173ec5b
  Guillaume Melquiond authored Sep 26, 2017
  
  5173ec5b
- Compile with -keep-locs to allow dead code analysis. · c72f763f
  Guillaume Melquiond authored Sep 26, 2017
  
  c72f763f
- Adapt to Coq 8.7. · 8e2ef3b8
  Guillaume Melquiond authored Sep 26, 2017
  
  8e2ef3b8
- Set logic to QF_AUFLIRA for Yices-smt2, as it will not even start parsing the input file otherwise. · 109ba0d4
  Guillaume Melquiond authored Aug 25, 2017
  
  109ba0d4
25 Sep, 2017 2 commits
- Extraction: comment out condition about modular extraction · 7943044d
  Mário Pereira authored Sep 25, 2017
  
  7943044d
- make explicit the warning message for induction_ty_lex · 8d4cf301
  MARCHE Claude authored Sep 25, 2017
  
  8d4cf301
22 Sep, 2017 1 commit
- OCaml printer: minor · 8d8c999f
  Mário Pereira authored Sep 22, 2017
  
  8d8c999f
21 Sep, 2017 1 commit
- Schorr-Waite: because of writting effects the four memory components must remain non-ghost · ebf69ea1
  Mário Pereira authored Sep 21, 2017
  
  ebf69ea1