From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Dec 2015 23:15:02 +0100 Subject: Proof using: do not clear unused section hyps automatically The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account. --- theories/Lists/List.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fe18686e2..443dd683d 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -970,6 +970,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 using A B. + clear Hfinjective. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. -- cgit v1.2.3