From fc0b90e4f8bc4f3c0781c517e433b6627cf6d730 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Nov 2016 15:44:39 +0100
Subject: [PATCH] Don't use Let outside of a section

---
 prelude/finite.v    | 4 +++-
 prelude/stringmap.v | 2 ++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/prelude/finite.v b/prelude/finite.v
index 3e6619852..3f4d0dd97 100644
--- a/prelude/finite.v
+++ b/prelude/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/prelude/stringmap.v b/prelude/stringmap.v
index f6eedf071..c9f23a1e2 100644
--- a/prelude/stringmap.v
+++ b/prelude/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.
-- 
GitLab