From 455b5b2672b972efd109be7c6d787e4f822e8b3a Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 1 Jun 2016 19:08:49 +0200 Subject: [PATCH] useless Arguments --- algebra/frac.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/algebra/frac.v b/algebra/frac.v index 84774bf2e..ad065890b 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. -- GitLab