Commits · e578ac608eda22f942ce9ab79619f78737ba625c · Rodolphe Lepigre / Iris

28 Feb, 2015 2 commits
- use less unexplainable flags for Coq · e578ac60
  Ralf Jung authored Feb 28, 2015
  
  e578ac60
- Eliminated w₀, valid₀ from robust safety. · f405f944
  David Swasey authored Feb 28, 2015
  
  f405f944
27 Feb, 2015 3 commits
- remove duplicate definition · e37fe58c
  Ralf Jung authored Feb 27, 2015
  
  e37fe58c
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · b7e659ec
  Ralf Jung authored Feb 27, 2015
  
  b7e659ec
- move wf_nat_ind to a common place · f5837771
  Ralf Jung authored Feb 27, 2015
  
  f5837771
26 Feb, 2015 10 commits
- One of the lifting lemmas. · 3d443698
  David Swasey authored Feb 27, 2015
  
  3d443698
- compile again · 8bd02d0f
  Ralf Jung authored Feb 26, 2015
  
  8bd02d0f
- make it finally, really possible to compile iris_core and MetricRec concurrently · cf4310ed
  Ralf Jung authored Feb 26, 2015
  
  cf4310ed
- make it all compile again · 380d3344
  Ralf Jung authored Feb 26, 2015
  
  380d3344
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · ede9a750
  Ralf Jung authored Feb 26, 2015
```
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 Feb 26, 2015
```
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 Feb 26, 2015
  
  5c33aedd
- try to play with (dist n) as equivalence relations... and quickly stop again... · 848ce08e
  Ralf Jung authored Feb 26, 2015
  
  848ce08e
- show that internal equality on discrete types is timeless · c750b189
  Ralf Jung authored Feb 26, 2015
  
  c750b189
- iris_meta comment · 548d2f7c
  Ralf Jung authored Feb 26, 2015
  
  548d2f7c
24 Feb, 2015 9 commits
- make it all work again by establishing our proof rules · c2d5b157
  Ralf Jung authored Feb 24, 2015
  
  c2d5b157
- reestablish our metalogical theorems · 74dcb506
  Ralf Jung authored Feb 24, 2015
  
  74dcb506
- give state_sat a more sane name · e9a299ed
  Ralf Jung authored Feb 24, 2015
  
  e9a299ed
- re-establish the well-definedness of our core logic · 25c7e78b
  Ralf Jung authored Feb 24, 2015
  
  25c7e78b
- we can have a BI over all resources, not just positive ones · 72d03c90
  Ralf Jung authored Feb 24, 2015
  
  72d03c90
- make sure we-regenerate the dependency information when the Makefile is changed · 070e2136
  Ralf Jung authored Feb 24, 2015
  
  070e2136
- break the dependency chain from iris_core to metric_rec · 5c453652
  Ralf Jung authored Feb 24, 2015
  
  5c453652
- make the Makefile compile the library correctly, and automatically find all the files · a11974b2
  Ralf Jung authored Feb 24, 2015
  
  a11974b2
- reorganize files for a more sane structure · 721698ac
  Ralf Jung authored Feb 24, 2015
  
  721698ac
23 Feb, 2015 7 commits
- use a gross hack to express diamond-shaped dependencies between the different parts of Iris · 04bab1dc
  Ralf Jung authored Feb 23, 2015
  
  04bab1dc
- remove unnecessary backticks · ca346a48
  Ralf Jung authored Feb 23, 2015
  
  ca346a48
- merge, merge, merge · aecd5422
  Janno authored Feb 23, 2015
  
  aecd5422
- heterogeneous products, homogeneous special case · 836300b2
  Janno authored Feb 23, 2015
  
  836300b2
- merge master with ra-constructions · 800af69d
  Janno authored Feb 23, 2015
  
  800af69d
- infprod RA: explain types · 8e069e6b
  Ralf Jung authored Feb 23, 2015
  
  8e069e6b
- removed superfluous instances of try · dc078e32
  Janno authored Feb 23, 2015
  
  dc078e32
22 Feb, 2015 1 commit
- Typo in statement of lift_pure_step. · c84fed03
  David Swasey authored Feb 22, 2015
  
  c84fed03
21 Feb, 2015 3 commits
- Got rid of iris_unsafe.v (htUnsafe in iris_wp.v, robust_safety in iris_meta.v). · a6d2564f
  David Swasey authored Feb 21, 2015
  
  a6d2564f
- Ownership is timeless. · 730a9f4a
  David Swasey authored Feb 21, 2015
  
  730a9f4a
- Notation and metavariables. · 9ba9ef1b
  David Swasey authored Feb 21, 2015
```
Moved connective notation to BI.

Added ⁺T for ra_pos T and eliminated BI.pres since I'd rather see ⁺res than BI.pres.

Bound mask_scope to type mask.
```
  9ba9ef1b
20 Feb, 2015 2 commits
- Cleaning up proofs · ba189cde
  Janno authored Feb 20, 2015
  
  ba189cde
- Agreement and infinite products on RAs · 7b2629db
  Janno authored Feb 20, 2015
  
  7b2629db
19 Feb, 2015 3 commits
- move equivP ro CSetoid as equivR · 0204cf5e
  Ralf Jung authored Feb 19, 2015
  
  0204cf5e
- no longer assume RA validity to be computable · 91bdb949
  Ralf Jung authored Feb 19, 2015
  
  91bdb949
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 417c45d8
  Ralf Jung authored Feb 19, 2015
  
  417c45d8