Commits · a838bd9450a553a5701bbb359d6af30eebe12c1b · Michael Sammler / iris-coq

Apr 24, 2018
- update CI · a838bd94
  Ralf Jung authored 6 years ago
  
  a838bd94
- use Lemma, not Let · 8f725f45
  Ralf Jung authored 6 years ago
  
  8f725f45
Apr 22, 2018
- Merge branch 'robbert/done_evar' into 'gen_proofmode' · 46cc91ed
  Ralf Jung authored 6 years ago
  
  Let `done` and friends fail when the proofmode goal is an evar. See merge request FP/iris-coq!140
  46cc91ed
- bump std++ · 840ce3af
  Ralf Jung authored 6 years ago
  
  840ce3af
- actually solve_proper can do this · e546ce9e
  Ralf Jung authored 6 years ago
  
  e546ce9e
Apr 21, 2018
- strengthen fixpoint non-expansiveness lemmas · 5a46ccf6
  Ralf Jung authored 6 years ago
  
  5a46ccf6
Apr 20, 2018
- Let `done` and friends fail when the proofmode goal is an evar. · fa0e8eb8
  Robbert Krebbers authored 6 years ago
  
  This fixes issue #182.
  fa0e8eb8
Apr 19, 2018
- make fixpoints simpl never · 78dedb27
  Ralf Jung authored 6 years ago
  
  78dedb27
- more mask-related fancy update lemmas · 67325634
  Ralf Jung authored 6 years ago
  
  67325634
- prove generally applicable lemmas for non-mask-matching fancy updates · d3412460
  Ralf Jung authored 6 years ago
  
  d3412460
Apr 18, 2018
- bump std++ to fix build · 55711e8e
  Ralf Jung authored 6 years ago
  
  55711e8e
- update CI · 84ee5362
  Ralf Jung authored 6 years ago
  
  84ee5362
- Merge remote-tracking branch 'origin/master' into gen_proofmode · 0c0f339e
  Ralf Jung authored 6 years ago
  
  0c0f339e
- test against Coq 8.8.0 · 5d40b106
  Ralf Jung authored 6 years ago
  
  5d40b106
- drop support for Coq 8.6; use the ssreflect that ships with Coq · ccb21344
  Ralf Jung authored 6 years ago
  
  ccb21344
- Revert most of "test against Coq 8.8.0, update CI" · 1c09a14c
  Ralf Jung authored 6 years ago
  
  This reverts commit 45162e5a. We have to wait until ssreflect makes an 8.8-compatible release.
  1c09a14c
- test against Coq 8.8.0; updated CI · 7adbdee1
  Ralf Jung authored 6 years ago
  
  7adbdee1
- test against Coq 8.8.0, update CI · 45162e5a
  Ralf Jung authored 6 years ago
  
  45162e5a
Apr 11, 2018
- Merge branch 'gmultiset' into 'master' · b6f03016
  Robbert Krebbers authored 6 years ago
  
  gmultiset RA See merge request FP/iris-coq!138
  b6f03016
- gmultiset RA · 638b445b
  Dan Frumin authored 6 years ago
  
  638b445b
- Bump the std++ version · a5ba9615
  Dan Frumin authored 6 years ago
  
  a5ba9615
Apr 10, 2018
- update CI · d7bd2bb5
  Ralf Jung authored 6 years ago
  
  d7bd2bb5
Apr 09, 2018
- Bump std++. · 5001567e
  Robbert Krebbers authored 6 years ago
  
  5001567e
- Merge branch 'robbert/embed_emp' into 'gen_proofmode' · cbe1f1ee
  Robbert Krebbers authored 6 years ago
  
  Weaken axioms for BI embeddings See merge request FP/iris-coq!137
  cbe1f1ee
- only run coqchk in one job · 31358801
  Ralf Jung authored 6 years ago
  
  31358801
- bump std++ · 7e33a806
  Ralf Jung authored 6 years ago
  
  7e33a806
- rename : affinely_persistently -> intuitionistically. Add lemma about... · 51dbb411
  Jacques-Henri Jourdan authored 6 years ago
  
  rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.
  51dbb411
- ofe_funC_ofe_discrete and ofe_funR_cmra_discrete. · 00b874ce
  Jacques-Henri Jourdan authored 6 years ago
  
  00b874ce
Apr 06, 2018
- update CI · 43416360
  Ralf Jung authored 6 years ago
  
  43416360
- move OPAM_PKG to the 8.8+beta1 job as that one is spawned first · 87135ffc
  Ralf Jung authored 6 years ago
  
  87135ffc
- also time against Coq 8.8 beta · b2581988
  Ralf Jung authored 6 years ago
  
  b2581988
- update std++ to make sure we have all notations around · 22631563
  Ralf Jung authored 6 years ago
  
  22631563
Apr 05, 2018
- Merge branch 'ralf/bi_disambig' into 'gen_proofmode' · e6c86a8d
  Ralf Jung authored 6 years ago
  
  add notation to define the PROP we use for a particular turnstile See merge request FP/iris-coq!134
  e6c86a8d
- fix notation conflict · 75e30fd5
  Ralf Jung authored 6 years ago
  
  75e30fd5
- make the annotated notations only parsing; add annotated versions of the curried forms (⊢) and (⊣⊢) · b3af10b3
  Ralf Jung authored 6 years ago
  
  b3af10b3
- add '@' to type ascription notation for disambiguation · e53c8a39
  Ralf Jung authored 6 years ago
  
  e53c8a39
- add notation to define the PROP we use for a particular turnstile · c0be693a
  Ralf Jung authored 7 years ago
  
  Fixes #156
  c0be693a
- Merge branch 'robbert/ElimModal' into 'gen_proofmode' · 44c5c039
  Robbert Krebbers authored 6 years ago
  
  Extend ElimModal with Boolean flags to specify whether it operates on the… See merge request FP/iris-coq!129
  44c5c039
Apr 04, 2018
- Separate type class for `■ ⎡P⎤ ⊢ ⎡■ P⎤`. · 09ae3206
  Robbert Krebbers authored 6 years ago
  
  09ae3206
- Remove embed emp axiom. · 9a745670
  Robbert Krebbers authored 6 years ago
  
  9a745670