Commit 455b5b26 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

useless Arguments

parent 62436505
Pipeline #1256 passed with stage
From Coq.QArith Require Import Qcanon. From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
From iris.algebra Require Import upred. From iris.algebra Require Import upred.
Local Arguments op _ _ !_ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Notation frac := Qp. Notation frac := Qp.
......
Markdown is supported
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