diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
| commit | 33742251e62a49c7996b96ca7077cf985627d14b (patch) | |
| tree | e75d9166f963fdfa21ab754e2c9471909143ac60 /theories/Lists | |
| parent | 7212e6c4a742110138a268650a59a67ef28d0582 (diff) | |
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.
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |