From 4219b955e54c07226128d6db51a3b33b24b3f5ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Jan 2018 11:27:48 -0800
Subject: [PATCH] Make `Forall_true` transparent.

This is needed so that it can be used be used as a combinator for defining
induction schemes for mutually inductive types.
---
 theories/list.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/list.v b/theories/list.v
index c685c985..5b028f24 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2175,7 +2175,7 @@ Section Forall_Exists.
     intros [??]; auto using Forall_app_2.
   Qed.
   Lemma Forall_true l : (∀ x, P x) → Forall P l.
-  Proof. induction l; auto. Qed.
+  Proof. intros ?. induction l; auto. Defined.
   Lemma Forall_impl (Q : A → Prop) l :
     Forall P l → (∀ x, P x → Q x) → Forall Q l.
   Proof. intros H ?. induction H; auto. Defined.
-- 
GitLab