diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v index f3842e4b8dbf7056cba1256573bf3d1ca9359a86..c6f43bfd0136b3dc526333fabd28f15ced891592 100644 --- a/theories/proofmode/monpred.v +++ b/theories/proofmode/monpred.v @@ -6,7 +6,7 @@ Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I) (P : monPred I PROP) (ð“Ÿ : PROP) := make_monPred_car : P i ⊣⊢ ð“Ÿ. Arguments MakeMonPredCar {_ _} _ _%I _%I. -Hint Mode MakeMonPredCar + + - ! -. +Hint Mode MakeMonPredCar + + - ! - : typeclass_instances. Section bi. Context {I : bi_index} {PROP : bi}.