From 376dff25c2314627e38944761fb19c463bbc331a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 20 Nov 2017 21:16:57 +0100
Subject: [PATCH] `Params` instance and correct the `Proper` for `fresh_list`.

---
 theories/collections.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 92fe98f7..a650917f 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -876,6 +876,8 @@ Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
   | 0 => []
   | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
   end.
+Instance: Params (@fresh_list) 6.
+
 Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
   | Forall_fresh_nil : Forall_fresh X []
   | Forall_fresh_cons x xs :
@@ -887,12 +889,9 @@ Section fresh.
 
   Global Instance fresh_proper: Proper ((≡) ==> (=)) (fresh (C:=C)).
   Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-  Global Instance fresh_list_proper:
-    Proper ((=) ==> (≡) ==> (=)) (fresh_list (C:=C)).
-  Proof.
-    intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal/=; [by rewrite E|].
-    apply IH. by rewrite E.
-  Qed.
+  Global Instance fresh_list_proper n:
+    Proper ((≡) ==> (=)) (fresh_list (C:=C) n).
+  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
 
   Lemma exist_fresh X : ∃ x, x ∉ X.
   Proof. exists (fresh X). apply is_fresh. Qed.
-- 
GitLab