From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Lists/List.v              | 42 +++++++++++++++++++++++---------------
 theories/Lists/ListDec.v           | 10 +++++----
 theories/Lists/ListSet.v           | 10 +++++----
 theories/Lists/ListTactics.v       | 10 +++++----
 theories/Lists/SetoidList.v        | 16 ++++++++-------
 theories/Lists/SetoidPermutation.v | 16 ++++++++-------
 theories/Lists/StreamMemo.v        | 10 +++++----
 theories/Lists/Streams.v           | 12 ++++++-----
 theories/Lists/vo.itarget          |  8 --------
 9 files changed, 75 insertions(+), 59 deletions(-)
 delete mode 100644 theories/Lists/vo.itarget

(limited to 'theories/Lists')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 30f1dec2..ca5f154e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Setoid.
@@ -27,7 +29,6 @@ Module ListNotations.
 Notation "[ ]" := nil (format "[ ]") : list_scope.
 Notation "[ x ]" := (cons x nil) : list_scope.
 Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope.
 End ListNotations.
 
 Import ListNotations.
@@ -419,7 +420,7 @@ Section Elts.
   Proof.
     unfold lt; induction n as [| n hn]; simpl.
     - destruct l; simpl; [ inversion 2 | auto ].
-    - destruct l as [| a l hl]; simpl.
+    - destruct l; simpl.
       * inversion 2.
       * intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -1280,7 +1281,7 @@ End Fold_Right_Recursor.
     partition l = ([], []) <-> l = [].
   Proof.
     split.
-    - destruct l as [|a l' _].
+    - destruct l as [|a l'].
       * intuition.
       * simpl. destruct (f a), (partition l'); now intros [= -> ->].
     - now intros ->.
@@ -2110,13 +2111,13 @@ Section Exists_Forall.
       {Exists l} + {~ Exists l}.
     Proof.
       intro Pdec. induction l as [|a l' Hrec].
-      - right. now rewrite Exists_nil.
+      - right. abstract now rewrite Exists_nil.
       - destruct Hrec as [Hl'|Hl'].
         * left. now apply Exists_cons_tl.
         * destruct (Pdec a) as [Ha|Ha].
           + left. now apply Exists_cons_hd.
-          + right. now inversion_clear 1.
-    Qed.
+          + right. abstract now inversion 1.
+    Defined.
 
     Inductive Forall : list A -> Prop :=
       | Forall_nil : Forall nil
@@ -2152,9 +2153,9 @@ Section Exists_Forall.
       - destruct Hrec as [Hl'|Hl'].
         + destruct (Pdec a) as [Ha|Ha].
           * left. now apply Forall_cons.
-          * right. now inversion_clear 1.
-        + right. now inversion_clear 1.
-    Qed.
+          * right. abstract now inversion 1.
+        + right. abstract now inversion 1.
+    Defined.
 
   End One_predicate.
 
@@ -2179,6 +2180,16 @@ Section Exists_Forall.
        * now apply Exists_cons_hd.
   Qed.
 
+  Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) :
+    (forall x:A, {P x} + { ~ P x }) ->
+    ~ Forall P l ->
+    Exists (fun x => ~ P x) l.
+  Proof.
+    intro Dec.
+    apply Exists_Forall_neg; intros.
+    destruct (Dec x); auto.
+  Qed.
+
   Lemma Forall_Exists_dec (P:A->Prop) :
     (forall x:A, {P x} + { ~ P x }) ->
     forall l:list A,
@@ -2186,9 +2197,8 @@ Section Exists_Forall.
   Proof.
     intros Pdec l.
     destruct (Forall_dec P Pdec l); [left|right]; trivial.
-    apply Exists_Forall_neg; trivial.
-    intro x. destruct (Pdec x); [now left|now right].
-  Qed.
+    now apply neg_Forall_Exists_neg.
+  Defined.
 
   Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
     forall l, Forall P l -> Forall Q l.
diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v
index 3e2eeac0..e7e2cfc8 100644
--- a/theories/Lists/ListDec.v
+++ b/theories/Lists/ListDec.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Decidability results about lists *)
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 655d3940..cc7d6f55 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** A library for finite sets, implemented as lists *)
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 537d5f68..843e3835 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import BinPos.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index c95fb4d5..0c5fe55b 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
 
 Require Export List.
 Require Export Sorted.
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index cea3e839..24b96514 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
 
 Require Import Permutation SetoidList.
 (* Set Universe Polymorphism. *)
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index 5a16cc43..57f558de 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import Eqdep_dec.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 1c302b22..8a01b8fb 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Set Implicit Arguments.
@@ -194,7 +196,7 @@ Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
 (map s)) S <-> ForAll P (map S).
 Proof.
 intros P S.
-split; generalize S; clear S; cofix; intros S; constructor;
+split; generalize S; clear S; cofix ForAll_map; intros S; constructor;
 destruct H as [H0 H]; firstorder.
 Qed.
 
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
deleted file mode 100644
index 82dd1be8..00000000
--- a/theories/Lists/vo.itarget
+++ /dev/null
@@ -1,8 +0,0 @@
-ListSet.vo
-ListTactics.vo
-List.vo
-ListDec.vo
-SetoidList.vo
-SetoidPermutation.vo
-StreamMemo.vo
-Streams.vo
-- 
cgit v1.2.3