From ab61aa61b1bb50f76101bb38ea5fe76eb1ea2244 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Sun, 28 Dec 2014 15:43:44 +0100 Subject: Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many section variable. For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context. --- theories/Lists/List.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c004b156b..fb686151b 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -969,7 +969,7 @@ Section Map. Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof. + Proof using A B. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. -- cgit v1.2.3