theories/decidable.v · 5ba352a350874dd3bdea8b4c8d632bb6442336eb · Arthur Azevedo de Amorim / stdpp

Forked from Iris / stdpp

Source project has a limited visibility.

5 years ago

Now we follow Coq's stdlib and declare this instance using a `Hint Extern`;
this avoids making `flip` type class opaque.

5ba352a3

Robbert Krebbers authored 5 years ago

Now we follow Coq's stdlib and declare this instance using a `Hint Extern`;
this avoids making `flip` type class opaque.