theories/listset.v → stdpp/listset.v

@@ -4,8 +4,8 @@ From stdpp Require Export sets list.
 From stdpp Require Import options.
 
 Record listset A := Listset { listset_car: list A }.
-Arguments listset_car {_} _ : assert.
-Arguments Listset {_} _ : assert.
+Global Arguments listset_car {_} _ : assert.
+Global Arguments Listset {_} _ : assert.
 
 Section listset.
 Context {A : Type}.
@@ -28,7 +28,7 @@ Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
 Proof.
   destruct X as [l]; split; [|by intros; simplify_eq/=].
   rewrite elem_of_equiv_empty; intros Hl.
-  destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
+  destruct l as [|x l]; [done|]. oinversion Hl. left.
 Qed.
 Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
 Proof.
@@ -48,7 +48,7 @@ Global Instance listset_intersection: Intersection (listset A) :=
 Global Instance listset_difference: Difference (listset A) :=
   λ '(Listset l) '(Listset k), Listset (list_difference l k).
 
-Instance listset_set: Set_ A (listset A).
+Local Instance listset_set: Set_ A (listset A).
 Proof.
   split.
   - apply _.
@@ -66,14 +66,14 @@ Proof.
 Qed.
 End listset.
 
-Instance listset_ret: MRet listset := λ A x, {[ x ]}.
-Instance listset_fmap: FMap listset := λ A B f '(Listset l),
+Global Instance listset_ret: MRet listset := λ A x, {[ x ]}.
+Global Instance listset_fmap: FMap listset := λ A B f '(Listset l),
   Listset (f <$> l).
-Instance listset_bind: MBind listset := λ A B f '(Listset l),
+Global Instance listset_bind: MBind listset := λ A B f '(Listset l),
   Listset (mbind (listset_car ∘ f) l).
-Instance listset_join: MJoin listset := λ A, mbind id.
+Global Instance listset_join: MJoin listset := λ A, mbind id.
 
-Instance listset_set_monad : MonadSet listset.
+Global Instance listset_set_monad : MonadSet listset.
 Proof.
   split.
   - intros. apply _.

theories/listset_nodup.v → stdpp/listset_nodup.v

@@ -7,9 +7,9 @@ From stdpp Require Import options.
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
 }.
-Arguments ListsetNoDup {_} _ _ : assert.
-Arguments listset_nodup_car {_} _ : assert.
-Arguments listset_nodup_prf {_} _ : assert.
+Global Arguments ListsetNoDup {_} _ _ : assert.
+Global Arguments listset_nodup_car {_} _ : assert.
+Global Arguments listset_nodup_prf {_} _ : assert.
 
 Section list_set.
 Context `{EqDecision A}.
@@ -29,7 +29,7 @@ Global Instance listset_nodup_difference: Difference C :=
   λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
     ListsetNoDup _ (NoDup_list_difference _ k Hl).
 
-Instance listset_nodup_set: Set_ A C.
+Local Instance listset_nodup_set: Set_ A C.
 Proof.
   split; [split | | ].
   - by apply not_elem_of_nil.

theories/orders.v → stdpp/orders.v

@@ -13,7 +13,7 @@ Section orders.
   Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
   Proof. by intros <-. Qed.
   Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
-  Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm _). Qed.
+  Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm R). Qed.
   Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
   Proof. done. Qed.
   Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.