theories/listset_nodup.v → stdpp/listset_nodup.v

@@ -2,14 +2,14 @@
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
 From stdpp Require Export sets list.
-Set Default Proof Using "Type".
+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.
@@ -41,5 +41,5 @@ Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance listset_nodup_fin_set: FinSet A C.
-Proof. split. apply _. done. by intros [??]. Qed.
+Proof. split; [apply _|done|]. by intros [??]. Qed.
 End list_set.

theories/prelude.v → stdpp/prelude.v

@@ -12,3 +12,4 @@ From stdpp Require Export
   list
   list_numbers
   lexico.
+From stdpp Require Import options.