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/options.v → stdpp/options.v

-(** Coq configuration for std++ (not meant to leak to clients) *)
+(** Coq configuration for std++ (not meant to leak to clients).
+If you are a user of std++, note that importing this file means
+you are implicitly opting-in to every new option we will add here
+in the future. We are *not* guaranteeing any kind of stability here.
+Instead our advice is for you to have your own options file; then
+you can re-export the std++ file there but if we ever add an option
+you disagree with you can easily overwrite it in one central location. *)
 (* Everything here should be [Export Set], which means when this
 file is *imported*, the option will only apply on the import site
 but not transitively. *)
 
-Export Set Default Proof Using "Type".
+(** Allow async proof-checking of sections. *)
+#[export] Set Default Proof Using "Type".
 (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
-Export Set Suggest Proof Using. *)
-Export Set Default Goal Selector "!".
+#[export] Set Suggest Proof Using. *)
+
+(** Enforces that every tactic is executed with a single focused goal, meaning
+that bullets and curly braces must be used to structure the proof. *)
+#[export] Set Default Goal Selector "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.