• Robbert Krebbers's avatar
    Avoid use of `solve_proper`. · c579b46c
    Robbert Krebbers authored
    Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
    instead of the version of std++. The version in std++ can inherently
    not solve this, so I changed it into a manual proof.
    c579b46c
Name
Last commit
Last update
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
descr Loading commit data...
opam Loading commit data...