coq-community / fav-ssr

Functional Algorithms Verified in SSReflect [maintainer=@clayrat]
MIT License
45 stars 7 forks source link

Switch to up_log #3

Closed clayrat closed 2 years ago

clayrat commented 2 years ago

Starting from 1.14, Mathcomp now has up_log and enough lemmas to use for e.g. bintrees instead of rolling our own.

clayrat commented 2 years ago

Closed in https://github.com/clayrat/fav-ssr/commit/8977922dd4d89333a811488423d6268da863680a