diff --git a/.gitignore b/.gitignore
index 1cc22fd6bd76a52389240d22d9d0635e2c06a91f..2445b5480744e4ffded8dee04b2a1fb7137f1917 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 0e3a671da9308f5794d6b1fdfb58cefee1459482..ec42bf3236b8562b57d72048d93e014d5d763917 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.