From f1e3d5f212b2483677d3427fdd951f100a3406bb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 13 May 2019 13:48:22 +0200
Subject: [PATCH] make as_fractional_fractional a useful instance
---
theories/bi/lib/fractional.v | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index f39225418..ec7b4666a 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}.
--
GitLab