Skip to content
Snippets Groups Projects
Commit 4179bb8a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`FromAnd` is never used for `iCombine`, so remove that mode.

parent 55e78d6f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/classes.v
+ 0
− 1
View file @ 4179bb8a
......@@ -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:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment