From 68f87208033e81b171a87c1c54ef170bd6f2caec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 6 Sep 2021 16:14:53 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)
---
theories/list.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/list.v b/theories/list.v
index c6e0aeb4..05465e2b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2713,7 +2713,7 @@ Proof.
Defined.
(** Export the Coq stdlib constructors under different names,
-because we use Forall_nil and Forall_cons for a version with a biimplication. *)
+because we use [Forall_nil] and [Forall_cons] for a version with a biimplication. *)
Definition Forall_nil_2 := @Forall_nil A.
Definition Forall_cons_2 := @Forall_cons A.
Global Instance Forall_proper:
@@ -2986,7 +2986,7 @@ Lemma Forall2_Forall {A} P (l1 l2 : list A) :
Proof. induction 1; constructor; auto. Qed.
(** Export the Coq stdlib constructors under a different name,
-because we use Forall_nil and Forall_cons for a version with a biimplication. *)
+because we use [Forall2_nil] and [Forall2_cons] for a version with a biimplication. *)
Definition Forall2_nil_2 := @Forall2_nil.
Definition Forall2_cons_2 := @Forall2_cons.
Section Forall2.
--
GitLab