Commit d9b128a7 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove `:>>` subclass instance declarations

There are not documented in
https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class,
and they don't have any advantage, so it's better to stop using them.
parent c6eed539
Pipeline #20946 passed with stage
in 10 minutes and 4 seconds
......@@ -1161,7 +1161,7 @@ Class SemiSet A C `{ElemOf A C,
}.
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
set_semi_set :>> SemiSet A C;
set_semi_set :> SemiSet A C;
elem_of_intersection (X Y : C) (x : A) : x X Y x X x Y;
elem_of_difference (X Y : C) (x : A) : x X Y x X x Y
}.
......@@ -1201,7 +1201,7 @@ Qed.
anyway so as to avoid cycles in type class search. *)
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_set_set :>> Set_ A C;
fin_set_set :> Set_ A C;
elem_of_elements (X : C) x : x elements X x X;
NoDup_elements (X : C) : NoDup (elements X)
}.
......
......@@ -11,8 +11,8 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
OMap M, Merge M, A, FinMapToList K A (M A), EqDecision K,
ElemOf K D, Empty D, Singleton K D,
Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M;
finmap_dom_set :>> Set_ K D;
finmap_dom_map :> FinMap K M;
finmap_dom_set :> Set_ K D;
elem_of_dom {A} (m : M A) i : i dom D m is_Some (m !! i)
}.
......
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