From 99be46eb50213d1f35dfc4d30f35760ad5e75621 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 1 Aug 2014 14:39:51 +0200
Subject: More proofs independent of the names generated by induction/elim over
 a dependent elimination principle for Prop arguments.

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

(limited to 'theories/Lists')

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 03c2222aa..f02c1d13f 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -116,7 +116,7 @@ Section first_definitions.
     simple induction x; simpl; intros.
     apply H0; red; trivial.
     case (Aeq_dec a a0); auto with datatypes.
-    intro; apply H; intros; auto.
+    intro Hneg; apply H; intros; auto.
     apply H1; red; intro.
     case H3; auto.
   Qed.
-- 
cgit v1.2.3