Commits · 52c96f45f2e5d82b695d6e7d1eaccd47287d92c5 · Michael Sammler / iris-coq

Jun 26, 2018
- don't check output on testsuite at all when running against 8.9 · 52c96f45
  Ralf Jung authored 6 years ago
  
  52c96f45
Jun 25, 2018
- prove a variant of wp_invariance that does not require finding fupd_intro_mask' · 1244bcfb
  Ralf Jung authored 6 years ago
  
  1244bcfb
- bump std++; test that we don't break setoid_rewrite · 42f0842f
  Ralf Jung authored 6 years ago
  
  42f0842f
- always use notypeclasses refine · df4beedf
  Ralf Jung authored 6 years ago
  
  df4beedf
Jun 22, 2018
- Merge branch 'master' into gen_proofmode · 38ba379f
  Ralf Jung authored 6 years ago
  
  38ba379f
- update CI · 6bb2f803
  Ralf Jung authored 6 years ago
  
  6bb2f803
- tweak README · 0cd25a7c
  Ralf Jung authored 6 years ago
  
  0cd25a7c
Jun 21, 2018
- Merge branch 'master' into gen_proofmode · f9fc75c6
  Ralf Jung authored 6 years ago
  
  f9fc75c6
- update CI to use perf · 476483bc
  Ralf Jung authored 6 years ago
  
  476483bc
- bump stdpp · 94b2c6c1
  Ralf Jung authored 6 years ago
  
  94b2c6c1
- handle language.of_val in solve_into_val · 8ca8b776
  Ralf Jung authored 6 years ago
  
  8ca8b776
- prettify printing a bit · 3961c1e8
  Ralf Jung authored 6 years ago
  
  3961c1e8
- get rid of to_val_is_Some' · 393f02ed
  Ralf Jung authored 6 years ago
  
  393f02ed
Jun 20, 2018
- print whether we are testing or creating reference output · e04c9826
  Ralf Jung authored 6 years ago
  
  e04c9826
- change the way we generate test reference files · dbf8321a
  Ralf Jung authored 6 years ago
  
  dbf8321a
- use lia instead of omega · 2f1ae293
  Ralf Jung authored 6 years ago
  
  2f1ae293
Jun 19, 2018
- attempt to fix tests timing · 700677ca
  Ralf Jung authored 6 years ago
  
  700677ca
- implement proper dependency tracking for test files · c0ca4709
  Ralf Jung authored 6 years ago
  
  c0ca4709
Jun 18, 2018
- Merge branch 'master' into gen_proofmode · 33f0c279
  Ralf Jung authored 6 years ago
  
  33f0c279
- backport heap_lang notation fix from gen_proofmode · d2147936
  Ralf Jung authored 6 years ago
  
  d2147936
- Merge branch 'ralf/into_val' into 'gen_proofmode' · a4731f4c
  Ralf Jung authored 6 years ago
  
  change IntoVal so that it is easier to use in specs See merge request FP/iris-coq!159
  a4731f4c
- change AsVal to be easier to use (like IntoVal) · 68965acf
  Ralf Jung authored 6 years ago
  
  68965acf
- change IntoVal so that it is easier to use in specs · 8e8c7228
  Ralf Jung authored 6 years ago
  
  8e8c7228
- make coercions explicit to improve readability · a2dab2fb
  Ralf Jung authored 6 years ago
  
  a2dab2fb
- test against Coq 8.8 development branch · 598b8449
  Ralf Jung authored 6 years ago
  
  598b8449
Jun 17, 2018
- comment for how we plan to generalize the WP notation if necessary · 3673d5fd
  Ralf Jung authored 6 years ago
  
  3673d5fd
Jun 16, 2018
- remove Pos.succ from proofmode unfold list by making a copy · 01c940bd
  Ralf Jung authored 6 years ago
  
  01c940bd
- improve and test iApply error message · 1c8a145a
  Ralf Jung authored 6 years ago
  
  1c8a145a
- Merge branch 'ralf/errors' into 'gen_proofmode' · 1471ae26
  Ralf Jung authored 6 years ago
  
  Improve and test more proof mode error messages See merge request FP/iris-coq!160
  1471ae26
- Merge branch 'robbert/big_sepL2' into 'gen_proofmode' · f510b666
  Robbert Krebbers authored 6 years ago
  
  Separating big operator over two lists. See merge request FP/iris-coq!158
  f510b666
- Tests for `big_sepL2`. · eb3283dc
  Robbert Krebbers authored 6 years ago
  
  eb3283dc
Jun 15, 2018
- test and fix some more proof mode error messages · 49f26fdc
  Ralf Jung authored 6 years ago
  
  49f26fdc
- Make Ltac helper function local · db57a33e
  Ralf Jung authored 6 years ago
  
  db57a33e
- Proof mode error messages: Print hypothesis name without [INamed] · b39f5a52
  Ralf Jung authored 6 years ago
  
  b39f5a52
- Proof mode class instances for `big_sepL2`. · 982a55c7
  Robbert Krebbers authored 6 years ago
  
  All those for `big_sepL` that hold.
  982a55c7
- Separating big operator over two lists. · 76812039
  Robbert Krebbers authored 6 years ago
  
  76812039
- Adding `%I` to printing of proof mode hypotheses. · d88d654b
  Robbert Krebbers authored 6 years ago
  
  We already do the same for the goal, this avoids some scope delimiters being displayed.
  d88d654b
- Use `IsCons` and `IsApp` more consistently. · e2ece00a
  Robbert Krebbers authored 6 years ago
  
  e2ece00a
- Move comment about `IsCons` and `IsApp`. · a3a4c80f
  Robbert Krebbers authored 6 years ago
  
  a3a4c80f
- More ▷ commute lemmas for big operators. · 7ab36303
  Robbert Krebbers authored 6 years ago
  
  7ab36303