Commits · f5854570054c72402766be84a1d533d08b47d3ac · Gaëtan Gilbert / Iris

Mar 24, 2018
- update CI: use centralized CI repo; submiting timing to coq-speed · f5854570
  Ralf Jung authored 7 years ago
  
  f5854570
Mar 22, 2018
- Merge remote-tracking branch 'origin/master' into gen_proofmode · fe155b62
  Ralf Jung authored 7 years ago
  
  fe155b62
- CI: test Coq 8.8 branch · 9ca430f6
  Ralf Jung authored 7 years ago
  
  9ca430f6
Mar 21, 2018
- verified compatibility with Coq 8.8 (CI coming later) · 7b0ad6cd
  Ralf Jung authored 7 years ago
  
  7b0ad6cd
- bump std++; no changes needed · 8ab26a68
  Ralf Jung authored 7 years ago
  
  8ab26a68
- Stop iFrame from introducing modalities · bcce68db
  Ralf Jung authored 7 years ago
  
  Fixes #176
  bcce68db
- move Frame instances to their own file · 458a6d45
  Ralf Jung authored 7 years ago
  
  458a6d45
- split class_instances into BI and SBI instanced · 528b255f
  Ralf Jung authored 7 years ago
  
  528b255f
- split derived_laws into BI and SBI laws · dfc4dca9
  Ralf Jung authored 7 years ago
  
  dfc4dca9
- move general BI things using the proofmode down into lib/ · c2a8bce0
  Ralf Jung authored 7 years ago
  
  c2a8bce0
- Merge branch 'ralf/intuitionistically' into 'gen_proofmode' · ef2adeb3
  Ralf Jung authored 7 years ago
  
  rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition See merge request FP/iris-coq!130
  ef2adeb3
- apply Robbert's feedback · ff398120
  Ralf Jung authored 7 years ago
  
  ff398120
Mar 20, 2018
- FromAffinely instance for intuitionistic modality · 861490f0
  Ralf Jung authored 7 years ago
  
  861490f0
- teach framing about the intuitionistic modality · 373feb82
  Ralf Jung authored 7 years ago
  
  373feb82
- add tons of instances for the intuitionistic modality · 50ef1cf4
  Ralf Jung authored 7 years ago
  
  50ef1cf4
Mar 19, 2018
- get rid of 2nd into_persistent_intuitionistically instance · dd987574
  Ralf Jung authored 7 years ago
  
  dd987574
- Merge branch 'ralf/valid' into 'gen_proofmode' · 93ef2352
  Ralf Jung authored 7 years ago
  
  rename valid -> emp_valid See merge request FP/iris-coq!131
  93ef2352
- update iIntoEmpValid docs · 803d4b3d
  Ralf Jung authored 7 years ago
  
  803d4b3d
- iIntoValid -> iIntoEmpValid · 42655ec9
  Ralf Jung authored 7 years ago
  
  42655ec9
- rename valid -> emp_valid · 526f472c
  Ralf Jung authored 7 years ago
  
  526f472c
- rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition · ee12aa64
  Ralf Jung authored 7 years ago
  
  ee12aa64
- Fix typo. · aac8c9ef
  Robbert Krebbers authored 7 years ago
  
  aac8c9ef
Mar 16, 2018
- Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode · b1ddcc68
  Ralf Jung authored 7 years ago
  
  b1ddcc68
- Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`. · 6c6d0d65
  Robbert Krebbers authored 7 years ago
  
  The old one is admissable. Thanks to @jtassaro and @jung.
  6c6d0d65
- rename env_persistent -> env_intuitionistic · d4dc9190
  Ralf Jung authored 7 years ago
  
  d4dc9190
Mar 15, 2018
- make the README less outdated · ba28c6fa
  Ralf Jung authored 7 years ago
  
  ba28c6fa
Mar 14, 2018
- fix a fluke · aae0efc9
  Ralf Jung authored 7 years ago
  
  aae0efc9
- typo · 48f44eb2
  Ralf Jung authored 7 years ago
  
  48f44eb2
- no idea why I would think this implies monotonicity... · 484b1a45
  Ralf Jung authored 7 years ago
  
  484b1a45
- pers-emp actually just needs `core ε = ε` · 56056f66
  Ralf Jung authored 7 years ago
  
  56056f66
Mar 13, 2018
- Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode · 07563f84
  Ralf Jung authored 7 years ago
  
  07563f84
- show that persistently is also another fixpoint · ceee7105
  Ralf Jung authored 7 years ago
  
  ceee7105
- Merge branch 'joe/fresh' into 'gen_proofmode' · 73178ea3
  Robbert Krebbers authored 7 years ago
  
  Store a counter in `Envs` to assign fresh names with `iFresh`. See merge request FP/iris-coq!128
  73178ea3
- Reorganize monpred.v and no longer upclose bupd and fupd. · 43ac11df
  Jacques-Henri Jourdan authored 7 years ago
  
  43ac11df
- iFresh: document the Ltac trick to force evaluation of the side-effect. · d7f627fd
  Joseph Tassarotti authored 7 years ago
  
  d7f627fd
Mar 12, 2018
- note that forall_2 would be derivable in a classical meta-logic · 5c639877
  Ralf Jung authored 7 years ago
  
  5c639877
- show that persistently and affinely-persistently are fixpoints of something · 8389920e
  Ralf Jung authored 7 years ago
  
  8389920e
- Coq future-compat: use qualified name for · cea60198
  Ralf Jung authored 7 years ago
  
  cea60198
- iFresh: Force start proof when iFresh is called. · ba8b9e94
  Joseph Tassarotti authored 7 years ago
  
  ba8b9e94
- Store a counter in to assign fresh names with . · 938ea90c
  Joseph Tassarotti authored 7 years ago
  
  938ea90c