stdpp/listset.v

@@ -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.

stdpp/mapset.v

@@ -109,11 +109,9 @@ Definition mapset_map_with {A B} (f : bool → A → option B)
     match x, y with
     | Some _, Some a => f true a | None, Some a => f false a | _, None => None
     end) mX.
+
 Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M :=
-  Mapset $ merge (λ x _,
-    match x with
-    | Some a => if f a then Some () else None | None => None
-    end) m (@empty (M A) _).
+  Mapset $ omap (λ a, if f a then Some () else None) m.
 
 Lemma lookup_mapset_map_with {A B} (f : bool → A → option B) X m i :
   mapset_map_with f X m !! i = m !! i ≫= f (bool_decide (i ∈ X)).
@@ -126,15 +124,18 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
   i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
 Proof.
   unfold mapset_dom_with, elem_of, mapset_elem_of.
-  simpl. rewrite lookup_merge, lookup_empty. destruct (m !! i) as [a|]; simpl.
+  simpl. rewrite lookup_omap. destruct (m !! i) as [a|]; simpl.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
-Local Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+
+Local Instance mapset_dom {A} : Dom (M A) (mapset M) := λ m,
+  Mapset $ fmap (λ _, ()) m.
 Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
-  split; try apply _. intros. unfold dom, mapset_dom, is_Some.
-  rewrite elem_of_mapset_dom_with; naive_solver.
+  split; try apply _. intros A m i.
+  unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
+  rewrite lookup_fmap. destruct (m !! i); naive_solver.
 Qed.
 End mapset.
 

stdpp/namespaces.v

@@ -4,7 +4,7 @@ From stdpp Require Import options.
 Definition namespace := list positive.
 Global Instance namespace_eq_dec : EqDecision namespace := _.
 Global Instance namespace_countable : Countable namespace := _.
-Typeclasses Opaque namespace.
+Global Typeclasses Opaque namespace.
 
 Definition nroot : namespace := nil.
 

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.

stdpp/pretty.v

@@ -113,7 +113,7 @@ Proof. apply _. Qed.
 Global Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
-  end%string.
+  end.
 Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
   unfold pretty, pretty_Z.

stdpp/stringmap.v

@@ -17,7 +17,7 @@ Let R {A} (s : string) (m : stringmap A) (n1 n2 : N) :=
 Lemma fresh_string_step {A} s (m : stringmap A) n x :
   m !! (s +:+ pretty n) = Some x → R s m (1 + n) n.
 Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
-Lemma fresh_string_R_wf {A} s (m : stringmap A) : wf (R s m).
+Lemma fresh_string_R_wf {A} s (m : stringmap A) : well_founded (R s m).
 Proof.
   induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs].
   specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2).