Commits · 87b459595a038589e48685a3e6a021bc0c0ccbf4 · Amin Timany / iris-coq · GitLab

Snippets Groups Projects

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
- avoid being a delta-reduction away from Setoid's equiv (WARNING: some stuff... · 8a5aef49
  Ralf Jung authored 10 years ago
  
  avoid being a delta-reduction away from Setoid's equiv (WARNING: some stuff doesn't compile anymore)
  8a5aef49
- Weaken res_sat: We'll always keep a physical state around. · 5c33aedd
  David Swasey authored 10 years ago
  
  5c33aedd
- try to play with (dist n) as equivalence relations... and quickly stop again... · 848ce08e
  Ralf Jung authored 10 years ago
  
  848ce08e
- show that internal equality on discrete types is timeless · c750b189
  Ralf Jung authored 10 years ago
  
  c750b189
- iris_meta comment · 548d2f7c
  Ralf Jung authored 10 years ago
  
  548d2f7c
Feb 24, 2015
- make it all work again by establishing our proof rules · c2d5b157
  Ralf Jung authored 10 years ago
  
  c2d5b157
- reestablish our metalogical theorems · 74dcb506
  Ralf Jung authored 10 years ago
  
  74dcb506
- give state_sat a more sane name · e9a299ed
  Ralf Jung authored 10 years ago
  
  e9a299ed
- re-establish the well-definedness of our core logic · 25c7e78b
  Ralf Jung authored 10 years ago
  
  25c7e78b
- we can have a BI over all resources, not just positive ones · 72d03c90
  Ralf Jung authored 10 years ago
  
  72d03c90
- make sure we-regenerate the dependency information when the Makefile is changed · 070e2136
  Ralf Jung authored 10 years ago
  
  070e2136
- break the dependency chain from iris_core to metric_rec · 5c453652
  Ralf Jung authored 10 years ago
  
  5c453652
- make the Makefile compile the library correctly, and automatically find all the files · a11974b2
  Ralf Jung authored 10 years ago
  
  a11974b2
- reorganize files for a more sane structure · 721698ac
  Ralf Jung authored 10 years ago
  
  721698ac
Feb 23, 2015
- use a gross hack to express diamond-shaped dependencies between the different parts of Iris · 04bab1dc
  Ralf Jung authored 10 years ago
  
  04bab1dc