From dcda6b161734cd30cd303742a8bab157c18f0e56 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Oct 2021 17:21:59 -0400
Subject: [PATCH] relax AsFractional Hint Mode

---
 iris/bi/lib/fractional.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 05dee6eea..ac13b5f79 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -14,9 +14,10 @@ Global Arguments AsFractional {_} _%I _%I _%Qp.
 
 Global Arguments fractional {_ _ _} _ _.
 
-Global Hint Mode AsFractional - + - - : typeclass_instances.
+Global Hint Mode AsFractional - ! - - : typeclass_instances.
 (* To make [as_fractional_fractional] a useful instance, we have to
-allow [q] to be an evar. *)
+allow [q] to be an evar. The head of [Φ] will always be a λ so ! is
+not a useful mode there. *)
 Global Hint Mode AsFractional - - + - : typeclass_instances.
 
 Section fractional.
-- 
GitLab