Commits · 673f0a14249b5b3be4d45b95c567526311c93707 · William Mansky / Iris

Jan 06, 2017
- add \Sigma for boxes; use a coercion for constant functors · 587cde16
  Ralf Jung authored 8 years ago
  
  587cde16
Jan 05, 2017
- program_logic: improve 'proof using' hint to be more minimal, more future-proof · fbf07f03
  Ralf Jung authored 8 years ago
  
  fbf07f03
Jan 04, 2017
- don't use Proof Using in a few files that get too many unnecessary annotations from this · fa25e2cc
  Ralf Jung authored 8 years ago
  
  fa25e2cc
- Correct stupid bug about interpretation scopes. · 53fe9f40
  Jacques-Henri Jourdan authored 8 years ago
  
  53fe9f40
Jan 03, 2017

make "make quick" quick by adding hints about the used section variables · 71abda4d

Ralf Jung authored 8 years ago

This patch was created using

find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

71abda4d

Dec 22, 2016
- move gen_heap to base_logic. It does not depend on WP or antyhing language-specific. · 61840d31
  Ralf Jung authored 8 years ago
  
  61840d31
Dec 15, 2016
- Move stuff out of sections that does not depend on the section variables. · 26ed8552
  Robbert Krebbers authored 8 years ago
  
  26ed8552
Dec 13, 2016
- Try to speed up framing with fractional. · ef5af56a
  Jacques-Henri Jourdan authored 8 years ago
  
  ef5af56a
Dec 12, 2016
- Add lemma gen_heap_dealloc. · 0cc2c6e0
  Robbert Krebbers authored 8 years ago
  
  0cc2c6e0
Dec 09, 2016
- move everything to subfolder theories/ · 6b8069fa
  Ralf Jung authored 8 years ago
  
  6b8069fa