From aae110fde27b85c1fe4c87b4cc80a4884830bbbb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Mar 2017 13:12:13 +0100
Subject: [PATCH] Fix Coq 8.5 build.

---
 theories/base.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 68278202..88031b3b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -937,7 +937,7 @@ Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
   split.
   - induction 1; simpl; auto.
-  - induction l; intros []; subst; constructor; auto.
+  - induction l; destruct 1; subst; constructor; auto.
 Qed.
 
 Inductive NoDup {A} : list A → Prop :=
-- 
GitLab