Commits · 96107d33f70968c1d3d6036d3294803ce5397b11 · Lennard Gäher / Iris

22 Jun, 2018 2 commits
- rerun CI · 96107d33
  Ralf Jung authored Jun 22, 2018
  
  96107d33
- rerun CI · 934acd0f
  Ralf Jung authored Jun 22, 2018
  
  934acd0f
21 Jun, 2018 6 commits
- Merge branch 'master' into gen_proofmode · f9fc75c6
  Ralf Jung authored Jun 21, 2018
  
  f9fc75c6
- update CI to use perf · 476483bc
  Ralf Jung authored Jun 21, 2018
  
  476483bc
- bump stdpp · 94b2c6c1
  Ralf Jung authored Jun 21, 2018
  
  94b2c6c1
- handle language.of_val in solve_into_val · 8ca8b776
  Ralf Jung authored Jun 21, 2018
  
  8ca8b776
- prettify printing a bit · 3961c1e8
  Ralf Jung authored Jun 21, 2018
  
  3961c1e8
- get rid of to_val_is_Some' · 393f02ed
  Ralf Jung authored Jun 21, 2018
  
  393f02ed
20 Jun, 2018 3 commits
- print whether we are testing or creating reference output · e04c9826
  Ralf Jung authored Jun 20, 2018
  
  e04c9826
- change the way we generate test reference files · dbf8321a
  Ralf Jung authored Jun 20, 2018
  
  dbf8321a
- use lia instead of omega · 2f1ae293
  Ralf Jung authored Jun 20, 2018
  
  2f1ae293
19 Jun, 2018 2 commits
- attempt to fix tests timing · 700677ca
  Ralf Jung authored Jun 19, 2018
  
  700677ca
- implement proper dependency tracking for test files · c0ca4709
  Ralf Jung authored Jun 19, 2018
  
  c0ca4709
18 Jun, 2018 7 commits
- Merge branch 'master' into gen_proofmode · 33f0c279
  Ralf Jung authored Jun 18, 2018
  
  33f0c279
- backport heap_lang notation fix from gen_proofmode · d2147936
  Ralf Jung authored Jun 18, 2018
  
  d2147936
- Merge branch 'ralf/into_val' into 'gen_proofmode' · a4731f4c
  Ralf Jung authored Jun 18, 2018
```
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 Jun 15, 2018
  
  68965acf
- change IntoVal so that it is easier to use in specs · 8e8c7228
  Ralf Jung authored Jun 14, 2018
  
  8e8c7228
- make coercions explicit to improve readability · a2dab2fb
  Ralf Jung authored Jun 18, 2018
  
  a2dab2fb
- test against Coq 8.8 development branch · 598b8449
  Ralf Jung authored Jun 18, 2018
  
  598b8449
17 Jun, 2018 1 commit
- comment for how we plan to generalize the WP notation if necessary · 3673d5fd
  Ralf Jung authored Jun 17, 2018
  
  3673d5fd
16 Jun, 2018 5 commits
- remove Pos.succ from proofmode unfold list by making a copy · 01c940bd
  Ralf Jung authored Jun 16, 2018
  
  01c940bd
- improve and test iApply error message · 1c8a145a
  Ralf Jung authored Jun 16, 2018
  
  1c8a145a
- Merge branch 'ralf/errors' into 'gen_proofmode' · 1471ae26
  Ralf Jung authored Jun 16, 2018
```
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 Jun 16, 2018
```
Separating big operator over two lists.

See merge request FP/iris-coq!158
```
  f510b666
- Tests for `big_sepL2`. · eb3283dc
  Robbert Krebbers authored Jun 15, 2018
  
  eb3283dc
15 Jun, 2018 14 commits
- test and fix some more proof mode error messages · 49f26fdc
  Ralf Jung authored Jun 15, 2018
  
  49f26fdc
- Make Ltac helper function local · db57a33e
  Ralf Jung authored Jun 15, 2018
  
  db57a33e
- Proof mode error messages: Print hypothesis name without [INamed] · b39f5a52
  Ralf Jung authored Jun 15, 2018
  
  b39f5a52
- Proof mode class instances for `big_sepL2`. · 982a55c7
  Robbert Krebbers authored Jun 15, 2018
```
All those for `big_sepL` that hold.
```
  982a55c7
- Separating big operator over two lists. · 76812039
  Robbert Krebbers authored Jun 14, 2018
  
  76812039
- Adding `%I` to printing of proof mode hypotheses. · d88d654b
  Robbert Krebbers authored Jun 15, 2018
```
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 Jun 15, 2018
  
  e2ece00a
- Move comment about `IsCons` and `IsApp`. · a3a4c80f
  Robbert Krebbers authored Jun 15, 2018
  
  a3a4c80f
- More ▷ commute lemmas for big operators. · 7ab36303
  Robbert Krebbers authored Jun 15, 2018
  
  7ab36303
- Add missing Import. · 58fdaa3e
  Robbert Krebbers authored Jun 15, 2018
  
  58fdaa3e
- Merge branch 'ralf/pm_red' into 'gen_proofmode' · 4d9e16ec
  Ralf Jung authored Jun 15, 2018
```
move the reduction control of the proofmode to its own file and tweak it

See merge request FP/iris-coq!150
```
  4d9e16ec
- Merge branch 'ci/robbert/overloaded_wp' into 'gen_proofmode' · e67181e6
  Robbert Krebbers authored Jun 15, 2018
```
Typeclass to overload WP notation.

See merge request FP/iris-coq!146
```
  e67181e6
- move the reduction control of the proofmode to its own file and tweak it · 3bd43113
  Ralf Jung authored Jun 15, 2018
```
* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors
```
  3bd43113
- Typeclass to overload WP notation. · f2a18f5a
  Robbert Krebbers authored May 09, 2018
  
  f2a18f5a