Commits · 03757caf56585ff17563de41e337ef216c8b8669 · Iris / stdpp

Oct 13, 2023
- Merge branch 'ralf/solve-proper-subrelation' into 'master' · 03757caf
  Ralf Jung authored 1 year ago
  
  solve_proper: add support for subrelation See merge request !495
  03757caf
- style tweaks · 87514dbe
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  87514dbe
- we do need mode ! and eassumption after all · bb39df76
  Ralf Jung authored 1 year ago
  
  with tests
  bb39df76
- changelog · 20aa2105
  Ralf Jung authored 1 year ago
  
  20aa2105
- try fast_reflexivity first, not last · 4d2b8870
  Ralf Jung authored 1 year ago
  
  4d2b8870
- factor flip cleaning into a tactic · 3705700a
  Ralf Jung authored 1 year ago
  
  and more comments
  3705700a
- move some tactic tests so they can be run with fewer things compiling · 1d5b61f3
  Ralf Jung authored 1 year ago
  
  1d5b61f3
- move flip handling to inside f_equiv and solve_proper_finish · f816088c
  Ralf Jung authored 1 year ago
  
  f816088c
- solve_proper: add support for subrelation · c842d7e2
  Ralf Jung authored 1 year ago
  
  c842d7e2
- Merge branch 'mthrow' into 'master' · 75a2c419
  Robbert Krebbers authored 1 year ago
  
  Add `MThrow` and replace `MGuard` See merge request !522
  75a2c419
Oct 12, 2023
- Add elem_of_mfail and set_unfold_elem_of_mfail · 24d4bcfb
  Thibaut Pérami authored 1 year ago
  
  24d4bcfb
- Update changelog for MThrow · 3f522a4f
  Thibaut Pérami authored 1 year ago
  
  3f522a4f
- Update comment · a18e35bb
  Adam authored 1 year ago and Thibaut Pérami committed 1 year ago
  
  a18e35bb
- Add comment justifying use of bind in lemmas · f7f98438
  Adam authored 1 year ago and Thibaut Pérami committed 1 year ago
  
  f7f98438
- Add changelog entries for MFail · 906c8880
  Adam authored 1 year ago and Thibaut Pérami committed 1 year ago
  
  906c8880
- Replace `MGuard` with `MFail` · daae68d1
  Adam authored 1 year ago and Thibaut Pérami committed 1 year ago
  
  daae68d1
- Merge branch 'robbert/tcsimpl' into 'master' · 47e0eddc
  Robbert Krebbers authored 1 year ago
  
  Add `TCSimpl` type class. See merge request !521
  47e0eddc
- Comment. · ab6bf9f9
  Robbert Krebbers authored 1 year ago
  
  ab6bf9f9
- CHANGELOG. · f162b8df
  Robbert Krebbers authored 1 year ago
  
  f162b8df
- Test case for `TCSimpl`. · df663290
  Robbert Krebbers authored 1 year ago
  
  df663290
- Add `TCSimpl` type class. · 903bfaa4
  Robbert Krebbers authored 1 year ago
  
  903bfaa4
Oct 11, 2023
- start new changelog section · f9f5b73b
  Ralf Jung authored 1 year ago
  
  f9f5b73b
- fix version support statement · c019b2fc
  Ralf Jung authored 1 year ago
  
  c019b2fc
- tag 1.9.0 release · 9084203e
  Ralf Jung authored 1 year ago
  
  coq-stdpp-1.9.0
  
  9084203e
- Merge branch 'master' into 'master' · 54ef9243
  Ralf Jung authored 1 year ago
  
  Release 1.9.0 See merge request !516
  54ef9243
- Add highlights, properly order names · 9a2497f2
  Johannes Hostert authored 1 year ago
  
  Verified
  
  9a2497f2
Oct 07, 2023
- Merge branch 'robbert/tceq_comment' into 'master' · a6387775
  Ralf Jung authored 1 year ago
  
  Improve comment of `TCEq`. See merge request !523
  a6387775
- Improve comment of `TCEq`. · 00010a4a
  Robbert Krebbers authored 1 year ago
  
  00010a4a
Oct 06, 2023
- Merge branch 'robbert/cons_equiv_inj' into 'master' · f76ff8d7
  Ralf Jung authored 1 year ago
  
  Add instance `cons_equiv_inj`. See merge request !520
  f76ff8d7
- CHANGELOG. · e7bba7bd
  Robbert Krebbers authored 1 year ago
  
  e7bba7bd
- Add instance `cons_equiv_inj`. · ac7d40a8
  Robbert Krebbers authored 1 year ago
  
  ac7d40a8
Oct 05, 2023
- Merge branch 'robbert/take_drop_app' into 'master' · c57a2eed
  Robbert Krebbers authored 1 year ago
  
  Rework lemmas for `take/drop` of an `++`: Closes #197 See merge request !518
  c57a2eed
- CHANGELOG tweak. · ffdc7802
  Ralf Jung authored 1 year ago
  
  ffdc7802
- CHANGELOG. · 4ece5004
  Robbert Krebbers authored 1 year ago
  
  4ece5004
- Make `take`/`drop` lemmas for `app` more uniform. · a390c805
  Robbert Krebbers authored 1 year ago
  
  a390c805
- Adapt changelog for 1.9.0 · 5cd9c4b5
  Johannes Hostert authored 1 year ago
  
  Verified
  
  5cd9c4b5
- Merge branch 'robbert/take_drop_reverse' into 'master' · 0de86dec
  Robbert Krebbers authored 1 year ago
  
  Add lemmas for `reverse` of `take`/`drop`. See merge request !517
  0de86dec
- Improve CHANGELOG. · f4d2074d
  Ralf Jung authored 1 year ago and Robbert Krebbers committed 1 year ago
  
  f4d2074d
- Add lemmas for `reverse` of `take`/`drop`. · 642e227d
  Robbert Krebbers authored 1 year ago
  
  642e227d
Oct 03, 2023
- Merge branch 'ralf/odestruct' into 'master' · 83c8fcbf
  Ralf Jung authored 1 year ago
  
  add odestruct and other "open term" tactics See merge request !512
  83c8fcbf