Another try at removing strings.length (!144) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Michael Sammler requested to merge ci/msammler/length into master 4 years ago

Apr 10, 2020
- another try · 66664b37
  Michael Sammler authored 4 years ago
  
  66664b37
Apr 08, 2020
- More testing. · 6c604e56
  Robbert Krebbers authored 5 years ago
  
  6c604e56
- `length` notation in `base` to also fix `length` in Coq ≤ 8.10. · dc849367
  Robbert Krebbers authored 5 years ago
  
  dc849367
- Use `Check` instead of `About` to hopefully have stable test output among Coq versions. · f3842eb3
  Robbert Krebbers authored 5 years ago
  
  f3842eb3
- Fix `Export` order for `length`. Remove `length` hack in strings. Add a test. · 7d981af6
  Robbert Krebbers authored 5 years ago
  
  7d981af6