Skip to content

I
Iron
Commit 95066b92 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix for Coq master.

parent 65ff62e6
Pipeline #14816 passed with stage
    in 5 minutes and 59 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 3 deletions
    theories/algebra/ufrac_auth.v
    View file @ 95066b92
    ......@@ -33,9 +33,8 @@ Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
    ◯ (Some (q,x)).
    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 "●?{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●?{ q } a").
    Notation "◯?{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯?{ 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