Commits · 7a28b549a25f48fc435ffa7d1c729d56fa96f555 · Amin Timany / iris-coq

Mar 13, 2015
- 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
- adjust ptrans implicits. · 2fecbc7b
  David Swasey authored 10 years ago
  
  2fecbc7b
- unit_min implicits. · 32411b97
  David Swasey authored 10 years ago
  
  32411b97
- Adjusted RA: implicits, _ in notation, and unnamed hypotheses. · 16f5b534
  David Swasey authored 10 years ago
  
  16f5b534
- Merged, and followed up a bit on d88dae1. · 13d66a5b
  David Swasey authored 10 years ago
  
  13d66a5b
- Corrected statement of robust safety. · e20c42e7
  David Swasey authored 10 years ago
  
  e20c42e7
Mar 03, 2015
- let's not reinvent iter · b89caf6d
  Ralf Jung authored 10 years ago
  
  b89caf6d
Mar 02, 2015
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 7513edd5
  Ralf Jung authored 10 years ago
  
  Conflicts: coq-ho/iris_ht_rules.v
  7513edd5
- remove context filling notation, to fix use of [[ and ]] in proof scripts · f8effe8d
  Ralf Jung authored 10 years ago
  
  f8effe8d
- Bullets. · 0c09e141
  David Swasey authored 10 years ago
  
  0c09e141
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · b21239a9
  David Swasey authored 10 years ago
  
  b21239a9
- Moved equality notes to iris_core. · 0f73a45f
  David Swasey authored 10 years ago
  
  0f73a45f
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · b1dc5d60
  Ralf Jung authored 10 years ago
  
  b1dc5d60
- add a file to check that we added to assumptions anywhere, accidentally · 2230c868
  Ralf Jung authored 10 years ago
  
  2230c868
- Notes on equality (temporary). · 27d9c01d
  David Swasey authored 10 years ago
  
  27d9c01d
Feb 28, 2015
- use less unexplainable flags for Coq · e578ac60
  Ralf Jung authored 10 years ago
  
  e578ac60
- Eliminated w₀, valid₀ from robust safety. · f405f944
  David Swasey authored 10 years ago
  
  f405f944
Feb 27, 2015
- remove duplicate definition · e37fe58c
  Ralf Jung authored 10 years ago
  
  e37fe58c
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · b7e659ec
  Ralf Jung authored 10 years ago
  
  b7e659ec
- move wf_nat_ind to a common place · f5837771
  Ralf Jung authored 10 years ago
  
  f5837771
Feb 26, 2015
- One of the lifting lemmas. · 3d443698
  David Swasey authored 10 years ago
  
  3d443698
- compile again · 8bd02d0f
  Ralf Jung authored 10 years ago
  
  8bd02d0f
- make it finally, really possible to compile iris_core and MetricRec concurrently · cf4310ed
  Ralf Jung authored 10 years ago
  
  cf4310ed
- make it all compile again · 380d3344
  Ralf Jung authored 10 years ago
  
  380d3344
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · ede9a750
  Ralf Jung authored 10 years ago
  
  Conflicts: coq-ho/iris_plog.v coq-ho/lib/ModuRes/BI.v
  ede9a750