Skip to content
Snippets Groups Projects
Select Git revision
  • ralf/options
  • master default protected
  • robbert/cbn
  • robbert/from_option
  • robbert/tc_opaque
  • coq-stdpp-1.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
12 results
Blame Permalink
Forked from Iris / stdpp
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    c579b46c
    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
    History
    Avoid use of `solve_proper`.
    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.