diff --git a/theories/finite.v b/theories/finite.v
index 682e28219f3d6427fe7c01fd98b683dabb678442..eb8b868eec3e4188c48c13adaa7ffdc92a2f73a3 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -294,12 +294,13 @@ Proof.
   rewrite app_length, fmap_length. auto.
 Qed.
 
-Let list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
+Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
   fix go n :=
   match n with
   | 0 => [[]↾eq_refl]
   | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
   end.
+
 Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
   {| enum := list_enum (enum A) n |}.
 Next Obligation.
@@ -325,6 +326,7 @@ Next Obligation.
     eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
   - rewrite elem_of_app. eauto.
 Qed.
+
 Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
 Proof.
   unfold card; simpl. induction n as [|n IH]; simpl; auto.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index 7050cddb503d12758ce163fa853cec8877cb43d8..426d392bfe0f3fa51b11f8f4d7d810f7333c61be 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -11,6 +11,7 @@ Notation stringmap := (gmap string).
 Notation stringset := (gset string).
 
 (** * Generating fresh strings *)
+Section stringmap.
 Local Open Scope N_scope.
 Let R {A} (s : string) (m : stringmap A) (n1 n2 : N) :=
   n2 < n1 ∧ is_Some (m !! (s +:+ pretty (n1 - 1))).
@@ -59,3 +60,4 @@ Fixpoint fresh_strings_of_set
      let x := fresh_string_of_set s X in
      x :: fresh_strings_of_set s n ({[ x ]} ∪ X)
   end%nat.
+End stringmap.