From 576e6a3ad02d10b4080cec6eac7733addff50521 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 29 Aug 2019 14:41:28 +0200 Subject: [PATCH] Tweak names in proof. --- theories/algebra/big_op.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v index ee57b0df..cb9109bf 100644 --- a/theories/algebra/big_op.v +++ b/theories/algebra/big_op.v @@ -128,11 +128,11 @@ Section list. Global Instance big_opL_ne n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> eq ==> dist n) (big_opL o (A:=A)). - Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. + Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Global Instance big_opL_proper' : Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡)) (big_opL o (A:=A)). - Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. + Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Lemma big_opL_consZ_l (f : Z → A → M) x l : ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (1 + k)%Z y. -- 2.26.2