Commits · c04340115fd62200e7f1b9341e31acd7e45540a0 · Tej Chajed / iris

"docs/iris.tex" did not exist on "f01811c1695e43d29bde4c4d0fb3489a4ffb0b5f"

Feb 12, 2016
- simplify our build instructions to just "make" · c0434011
  Ralf Jung authored 9 years ago
  
  thanks to Christian Doczkal <doczkal@ps.uni-saarland.de> for the Makefile snippet!
  c0434011
Jan 21, 2016
- remove the generated Makefile, add a configure script generating it instead · d543c264
  Ralf Jung authored 9 years ago
  
  d543c264
- have a makefile · 1e241e13
  Ralf Jung authored 9 years ago
  
  1e241e13
Mar 24, 2015
- add target "make lib" to build only the library · 6e7d84ad
  Ralf Jung authored 9 years ago
  
  6e7d84ad
Feb 28, 2015
- use less unexplainable flags for Coq · e578ac60
  Ralf Jung authored 10 years ago
  
  e578ac60
Feb 24, 2015
- make sure we-regenerate the dependency information when the Makefile is changed · 070e2136
  Ralf Jung authored 10 years ago
  
  070e2136
- 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
Feb 21, 2015
- Got rid of iris_unsafe.v (htUnsafe in iris_wp.v, robust_safety in iris_meta.v). · a6d2564f
  David Swasey authored 10 years ago
  
  a6d2564f
Feb 15, 2015
- create iris_meta file for meta-theorems (adequacy, lifting lemmas). formulate... · 4bec9617
  Ralf Jung authored 10 years ago
  
  create iris_meta file for meta-theorems (adequacy, lifting lemmas). formulate two of our four lifting lemmas.
  4bec9617
Feb 05, 2015
- Proved htUnsafe. · 56b35361
  David Swasey authored 10 years ago
  
  56b35361
Feb 01, 2015
- complete reorganizing Coq · fcbf8d58
  Ralf Jung authored 10 years ago
  
  fcbf8d58
- get rid of the "inner" module, use an opaque WorldProp instead · 2ad23105
  Ralf Jung authored 10 years ago
  
  2ad23105
- make it all compile with an opaque world-prop · 5b22c4cf
  Ralf Jung authored 10 years ago
  
  5b22c4cf
Jan 31, 2015
- write an interface to world_prop, and make iris_core (assertion logic + world... · 758ad9f5
  Ralf Jung authored 10 years ago
  
  write an interface to world_prop, and make iris_core (assertion logic + world satisfaction) work with it
  758ad9f5
Oct 07, 2014
- Fixed a bug introduced by 8.4pl4 coq_makefile ("all" target arguments reversed). · f07179bc
  Filip Sieczkowski authored 10 years ago
  
  f07179bc
- More README, renamed library to ModuRes · 61f3b3f5
  Filip Sieczkowski authored 10 years ago
  
  61f3b3f5
Jul 06, 2014
- add makefile to coq-ho · 688d3287
  Ralf Jung authored 10 years ago
  
  688d3287
May 28, 2014
- Added a library for solving recursive domain equations. · 3d69aaa0
  Filip Sieczkowski authored 10 years ago
  
  3d69aaa0