Skip to content

S
stdpp
Commit b938e033 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Make `fresh` stuff `simpl never`. 

This fixes an issue in orc11.
parent 7b80dd85
Pipeline #15197 passed with stage
    in 8 minutes and 33 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 0 deletions
    theories/base.v
    View file @ b938e033
    ......@@ -1226,12 +1226,14 @@ aforementioned [fresh] function on finite sets that respects set equality. *)
    Class Fresh A C := fresh: C → A.
    Hint Mode Fresh - ! : typeclass_instances.
    Instance: Params (@fresh) 3 := {}.
    Arguments fresh : simpl never.
    Class Infinite A := {
    infinite_fresh :> Fresh A (list A);
    infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
    infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
    }.
    Arguments infinite_fresh : simpl never.
    (** * Miscellaneous *)
    Class Half A := half: A → 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