diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v index b13aa6abd16de876b7ae3d8180703e339b191f10..9596b66ca70b699751406e13b1d04d67cf288809 100644 --- a/iris/proofmode/classes.v +++ b/iris/proofmode/classes.v @@ -180,7 +180,6 @@ Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P. Global Arguments FromAnd {_} _%I _%I _%I : simpl never. Global Arguments from_and {_} _%I _%I _%I {_}. Global Hint Mode FromAnd + ! - - : typeclass_instances. -Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *) (** The [IntoAnd p P Q1 Q2] class is used to handle some [[H1 H2]] intro patterns: