Commits · ralf/hint-mode-plus · Iris / stdpp

Dec 15, 2022
- Derive keys. · 09a53f1f
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  09a53f1f
- Also use + for monad. · 1534af50
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  1534af50
- Fix some real ambiguities. · 3aaeed9c
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  3aaeed9c
- Consistent pattern for functional dependencies. · 65017a1c
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  65017a1c
- Hacks; might be due to a Coq bug. · 94d96758
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  94d96758
- Use ! for classes with "functional dependency". · 1390f476
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  1390f476
- make Type params mode + · da340de2
  Ralf Jung authored 2 years ago and Ralf Jung committed 2 years ago
  
  da340de2
Nov 30, 2022
- bump CI to Coq 8.16.1 · 8bf7243a
  Ralf Jung authored 2 years ago
  
  8bf7243a
- Merge branch 'robbert/issue_161' into 'master' · ffa862a8
  Ralf Jung authored 2 years ago
  
  Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`. See merge request !428
  ffa862a8
Nov 29, 2022
- Merge branch 'ralf/solve_ndisj' into 'master' · 4763d18a
  Ralf Jung authored 2 years ago
  
  make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y' See merge request !427
  4763d18a
- Move. · 9236a721
  Robbert Krebbers authored 2 years ago
  
  9236a721
- make sure this solves the goal · ba3c17be
  Ralf Jung authored 2 years ago
  
  ba3c17be
- Apply 2 suggestion(s) to 2 file(s) · 6aa72baa
  Ralf Jung authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  6aa72baa
- Merge branch 'robbert/tc_notypeclasses_refine' into 'master' · c984afe2
  Ralf Jung authored 2 years ago
  
  Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`. See merge request !426
  c984afe2
- linebreaks · 807bed4b
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  807bed4b
- CHANGELOG entry. · 8e824e47
  Robbert Krebbers authored 2 years ago
  
  8e824e47
- Add some tests. · ca55de72
  Robbert Krebbers authored 2 years ago
  
  ca55de72
- Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`. · 13287fd5
  Robbert Krebbers authored 2 years ago
  
  13287fd5
Nov 25, 2022
- add another testcase from iris.program_logic.atomic · da9205f9
  Ralf Jung authored 2 years ago
  
  da9205f9
- make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y' · 81766ef4
  Ralf Jung authored 2 years ago
  
  81766ef4
Nov 24, 2022
- Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`. · 3beca691
  Robbert Krebbers authored 2 years ago
  
  3beca691
- Merge branch 'robbert/tc_solve' into 'master' · d4458085
  Robbert Krebbers authored 2 years ago
  
  Add tactic `tc_solve`. See merge request !425
  d4458085
- CHANGELOG. · efa1b8f0
  Robbert Krebbers authored 2 years ago
  
  efa1b8f0
- Add tactic `tc_solve`. · 2db407d6
  Robbert Krebbers authored 2 years ago
  
  2db407d6
Nov 23, 2022
- Merge branch 'msammler/bv_simplify_fix' into 'master' · d40a9005
  Michael Sammler authored 2 years ago
  
  Fix unfolding logic of bv_simplify See merge request !411
  d40a9005
Nov 18, 2022
- Merge branch 'robbert/set_solver_eauto' into 'master' · 3a32d06d
  Robbert Krebbers authored 2 years ago
  
  Use `eauto` as default for `set_solver`. See merge request !420
  3a32d06d
- CHANGELOG. · 9091657c
  Robbert Krebbers authored 2 years ago
  
  9091657c
- Use `eauto` as default for `set_solver`. · b37cd70f
  Robbert Krebbers authored 2 years ago
  
  b37cd70f
- Merge branch 'gset_to_gmap_to_list' into 'master' · a00e9041
  Ralf Jung authored 2 years ago
  
  add gset_to_gmap_to_list See merge request !422
  a00e9041
Nov 17, 2022
- fix readme and CI ordering · d06ae4b9
  Ralf Jung authored 2 years ago
  
  d06ae4b9
- test Coq 8.16.0 · ba28c82b
  Ralf Jung authored 2 years ago
  
  ba28c82b
Nov 16, 2022
- rename lemma · 0c776fcd
  Ralf Jung authored 2 years ago
  
  0c776fcd
- remove some parentheses · 23c0883b
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  23c0883b
- Merge branch 'robbert/no_native_compiler' into 'master' · c25b43ed
  Robbert Krebbers authored 2 years ago
  
  Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`. See merge request !419
  c25b43ed
- Add comment. · 38b9f596
  Robbert Krebbers authored 2 years ago
  
  38b9f596
- add gset_to_gmap_to_list · 241a5563
  Ralf Jung authored 2 years ago
  
  241a5563
Nov 15, 2022
- clarify that the unstable package needs a dev version · b863c6ef
  Ralf Jung authored 2 years ago
  
  b863c6ef
Nov 02, 2022
- Merge branch 'msammler/coq_16748' into 'master' · c59b6199
  Ralf Jung authored 2 years ago
  
  Fix bitvector tests for coq#16748 See merge request !421
  c59b6199
- Fix bitvector tests for coq#16748 · eb662f83
  Michael Sammler authored 2 years ago
  
  eb662f83
Oct 20, 2022
- Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`. · 9fd57032
  Robbert Krebbers authored 2 years ago
  
  9fd57032