diff --git a/algebra/frac.v b/algebra/frac.v index 84774bf2e292d78ee2f98e919a9baefb75135a68..ad065890bf534d4a600121f3af29e8c1dd2fd8b2 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -1,9 +1,6 @@ From Coq.QArith Require Import Qcanon. From iris.algebra Require Export cmra. From iris.algebra Require Import upred. -Local Arguments op _ _ !_ !_ /. -Local Arguments validN _ _ _ !_ /. -Local Arguments valid _ _ !_ /. Notation frac := Qp.