diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v index f3922541879ffab40c04aef17fa8929fed9e0f0a..ec7b4666ac4e3ba9b1dc67ff1908d1eca9301c72 100644 --- a/theories/bi/lib/fractional.v +++ b/theories/bi/lib/fractional.v @@ -15,7 +15,9 @@ Arguments AsFractional {_} _%I _%I _%Qp. Arguments fractional {_ _ _} _ _. Hint Mode AsFractional - + - - : typeclass_instances. -Hint Mode AsFractional - - + + : typeclass_instances. +(* To make [as_fractional_fractional] a useful instance, we have to +allow [q] to be an evar. *) +Hint Mode AsFractional - - + - : typeclass_instances. Section fractional. Context {PROP : bi}.