Skip to content

I
Iris
Commit 265c2a13 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix compilation with Coq master.

parent e65b06a7
Pipeline #17364 passed with stage
    in 13 minutes and 37 seconds
    Show whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 2 deletions
    theories/algebra/ufrac_auth.v
    View file @ 265c2a13
    ......@@ -41,8 +41,8 @@ Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
    Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
    Instance: Params (@ufrac_auth_auth) 2.
    Instance: Params (@ufrac_auth_frag) 2.
    Instance: Params (@ufrac_auth_auth) 2 := {}.
    Instance: Params (@ufrac_auth_frag) 2 := {}.
    Notation "●U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●U{ q } a").
    Notation "◯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯U{ q } a").
    ......
    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