Commits · 3c4a0be0d0d26f3556f2f6f2ea6c880ff95fb235 · Amin Timany / iris-coq

Mar 18, 2015
- more *oops* · 3c4a0be0
  Ralf Jung authored 10 years ago
  
  3c4a0be0
- *oops* · 80173905
  Ralf Jung authored 10 years ago
  
  80173905
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · e99d76c3
  Ralf Jung authored 10 years ago
  
  e99d76c3
- port all the base rules to be about wp, pvs only · e09c5897
  Ralf Jung authored 10 years ago
  
  e09c5897
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · b6eafef5
  Janno authored 10 years ago
  
  b6eafef5
- algèbre des ressources pour les fonctions finis partielles · d2362016
  Janno authored 10 years ago
  
  d2362016
- pointwise composition of fin. funs · b6d6c258
  Janno authored 10 years ago
  
  b6d6c258
Mar 17, 2015
- some comments for clarity · 314df5df
  Ralf Jung authored 10 years ago
  
  314df5df
- fix iris_check · 6888e730
  Ralf Jung authored 10 years ago
  
  6888e730
- prove some hoare triple rules directly in terms of weakest pre · 0d548bb8
  Ralf Jung authored 10 years ago
  
  0d548bb8
Mar 16, 2015
- prove all view shift lemmas in terms of pvs · 8f1f393f
  Ralf Jung authored 10 years ago
  
  8f1f393f
- provie another way to prove pvs · f368d488
  Ralf Jung authored 10 years ago
  
  f368d488
- show that safeExpr makes sense · 44685c87
  Ralf Jung authored 10 years ago
  
  44685c87
- also lift monoid steps (and not just monoid updates) to view shifts · fbc4c09e
  Ralf Jung authored 10 years ago
  
  fbc4c09e
- prove all the missing three lifting lemmas · ac8bcdd4
  Ralf Jung authored 10 years ago
  
  ac8bcdd4
- prove the derived lemma for stateless lifting · 95049432
  Ralf Jung authored 10 years ago
  
  95049432
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 6ee08fec
  Ralf Jung authored 10 years ago
  
  6ee08fec
- prove the stateless lifting lemma · a9822fd0
  Ralf Jung authored 10 years ago
  
  a9822fd0
Mar 13, 2015
- Duplicate notation. · 5047fbad
  David Swasey authored 10 years ago
  
  5047fbad
- Parens. · 7189834c
  David Swasey authored 10 years ago
  
  7189834c
- domeq implicits. · 5781ff2a
  David Swasey authored 10 years ago
  
  5781ff2a
- lang implicits. · 77cf0344
  David Swasey authored 10 years ago
  
  77cf0344
- uni_pred implicits. · bcc17ae1
  David Swasey authored 10 years ago
  
  bcc17ae1
- extend_sub, extend_dist implicits. · a7167e19
  David Swasey authored 10 years ago
  
  a7167e19
- met_morph_nonexp implicits. · 7a28b549
  David Swasey authored 10 years ago
  
  7a28b549
- fdRemove_neq implicits. · ff65f6d8
  David Swasey authored 10 years ago
  
  ff65f6d8
- mu_mono implicits. · 144584f3
  David Swasey authored 10 years ago
  
  144584f3
- Frame-preserving updates and auth (other junk in RAMorph). · aa186b57
  David Swasey authored 10 years ago
  
  aa186b57
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 1f18a351
  David Swasey authored 10 years ago
  
  1f18a351
- iris_check.v now imports derived_rules · 47c2811b
  Janno authored 10 years ago
  
  47c2811b
- Fixed section name · cb6b2424
  Janno authored 10 years ago
  
  cb6b2424
Mar 12, 2015
- move stuff around a bit · bfda839c
  Ralf Jung authored 10 years ago
  
  bfda839c
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · f7d72048
  David Swasey authored 10 years ago
  
  f7d72048
Mar 11, 2015
- Merge branch 'misc' of git.fp.mpi-sws.org:nowbook · 2e710cc6
  Jan-Oliver Kaiser authored 10 years ago
  
  2e710cc6
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 2fdc5698
  Jan-Oliver Kaiser authored 10 years ago
  
  2fdc5698
- proved vs lemmas with new pvs lemmas · 62213f3f
  Jan-Oliver Kaiser authored 10 years ago
  
  62213f3f
Mar 08, 2015
- ra_res_ex renamed ex. · d994e178
  David Swasey authored 10 years ago
  
  d994e178
Mar 06, 2015
- drastically reduce the number of Arguments · c1329cc0
  Ralf Jung authored 10 years ago
  
  c1329cc0
Mar 05, 2015
- Instances for pcmprod_map [PreoMet.v] · 3d0b33f5
  Janno authored 10 years ago
  
  3d0b33f5
Mar 04, 2015
- Changed definition of pure to eliminate pointless proof obligations. · 87b45959
  David Swasey authored 10 years ago
  
  87b45959