Commits · 6f122df42a3670ad42dbb849809dafda12bc1ad8 · Abhishek Anand / Iris

Apr 04, 2018
- update CI · 6f122df4
  Ralf Jung authored 6 years ago
  
  6f122df4
Apr 03, 2018
- Merge branch 'ralf/lemma_rename' into 'gen_proofmode' · 9d68507d
  Ralf Jung authored 6 years ago
  
  more consistent lemma naming See merge request FP/iris-coq!135
  9d68507d
Mar 24, 2018
- update CI · c403f3cd
  Ralf Jung authored 7 years ago
  
  c403f3cd
- Merge remote-tracking branch 'origin/master' into gen_proofmode · ebbe0df0
  Ralf Jung authored 7 years ago
  
  ebbe0df0
- update CI · 88d2204f
  Ralf Jung authored 7 years ago
  
  88d2204f
- update CI: use centralized CI repo; submiting timing to coq-speed · f5854570
  Ralf Jung authored 7 years ago
  
  f5854570
- gitlab-extract: show which commit the bad line was in · 658c756f
  Ralf Jung authored 7 years ago
  
  658c756f
- update CI · f2b0a849
  Ralf Jung authored 7 years ago
  
  f2b0a849
- update CI · 67f3284b
  Ralf Jung authored 7 years ago
  
  67f3284b
- gitlab-extract: add support for excluding a branch · 7eb3534d
  Ralf Jung authored 7 years ago
  
  7eb3534d
- update CI · a5f0e7d8
  Ralf Jung authored 7 years ago
  
  a5f0e7d8
- we can't use variables in 'only:', so go back to OPAM_PKG_BRANCH · 812e9c44
  Ralf Jung authored 7 years ago
  
  812e9c44
- update CI: use dedicated buildjob script, submit timing information to coq-speed · 2cc7b4d8
  Ralf Jung authored 7 years ago
  
  2cc7b4d8
- CI needs submodules now · 5361ad82
  Ralf Jung authored 7 years ago
  
  5361ad82
- move CI scripts to submodule · a44b4c8c
  Ralf Jung authored 7 years ago
  
  a44b4c8c
Mar 22, 2018
- Merge remote-tracking branch 'origin/master' into gen_proofmode · fe155b62
  Ralf Jung authored 7 years ago
  
  fe155b62
- more consistent lemma naming · 0c4a3e1b
  Ralf Jung authored 7 years ago
  
  Fixes #177
  0c4a3e1b
- 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