From 6696fb9c5d13a30ea1755591713ab31ddaee7e9b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Dec 2017 17:34:31 +0100
Subject: [PATCH] fix build

---
 .gitignore             | 1 +
 theories/bi/fixpoint.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 1cc22fd6b..2445b5480 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,6 +8,7 @@
 .\#*
 *~
 *.bak
+.coqdeps.d
 .coq-native/
 build-dep/
 Makefile.coq
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index 0e3a671da..ec42bf323 100644
--- a/theories/bi/fixpoint.v
+++ b/theories/bi/fixpoint.v
@@ -67,7 +67,7 @@ Section least.
 End least.
 
 Section greatest.
-  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
+  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Global Instance greatest_fixpoint_ne : NonExpansive (bi_greatest_fixpoint F).
   Proof. solve_proper. Qed.
-- 
GitLab