Commits · 6bbd8f91170e5c8669f247e7f50583e292011557 · Amin Timany / iris-coq

Mar 19, 2015
- degrade some priorities · 6bbd8f91
  Ralf Jung authored 10 years ago
  
  6bbd8f91
- move the things that are only needed for the category-theoretic part... · ac137a9f
  Ralf Jung authored 10 years ago
  
  move the things that are only needed for the category-theoretic part (including bundled types) to CatBasics.v
  ac137a9f
- make it compile again · 25a56a21
  Ralf Jung authored 10 years ago
  
  25a56a21
- Track changes to Predom. · 0c3f0336
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  0c3f0336
- Support rewriting under RA constructors; the rewrites in OrdTests, ExTests, AuthTests used to fail. · eb7c460b
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  eb7c460b
- Rewrite both ways. · b53816ac
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  b53816ac
- Track changes to Predom. · 1bd4afc4
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  1bd4afc4
- Oops, arguments. · 4a6c7ca1
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  4a6c7ca1
- Rewriting under pord (see the ProdTest section). · f3f99374
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  f3f99374
- Protect resp_set from SSR. · 730c2860
  David Swasey authored 10 years ago and Ralf Jung committed 10 years ago
  
  730c2860
- ++explicit types · 9c413c19
  Ralf Jung authored 10 years ago
  
  9c413c19
- more explicit variance annotations; why do we have two extensible_prod constructions? · e6b1e0dc
  Ralf Jung authored 10 years ago
  
  e6b1e0dc
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