From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 theories/Program/Basics.v      |  2 +-
 theories/Program/Combinators.v |  2 +-
 theories/Program/Equality.v    |  4 ++--
 theories/Program/Program.v     |  2 +-
 theories/Program/Subset.v      | 14 +++++++-------
 theories/Program/Syntax.v      |  2 +-
 theories/Program/Tactics.v     |  2 +-
 theories/Program/Utils.v       |  2 +-
 theories/Program/Wf.v          | 23 +++++++++++------------
 9 files changed, 26 insertions(+), 27 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 2c0f62ad..e5be0ca9 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 4d631e78..e246041b 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 04701ff5..a9aa30df 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -263,7 +263,7 @@ Class DependentEliminationPackage (A : Type) :=
 
 Ltac elim_tac tac p :=
   let ty := type of p in
-  let eliminator := eval simpl in (elim (A:=ty)) in
+  let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in
     tac p eliminator.
 
 (** Specialization to do case analysis or induction.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 38f11231..5af6f4d7 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 269556c2..50b89b5c 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -61,12 +61,12 @@ Ltac pi_subset_proofs := repeat pi_subset_proof.
 Ltac clear_subset_proofs :=
   abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups.
 
-Ltac pi := repeat progress f_equal ; apply proof_irrelevance.
+Ltac pi := repeat f_equal ; apply proof_irrelevance.
 
 Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
 Proof.
-  induction n.
-  induction m.
+  destruct n as (x,p).
+  destruct m as (x',p').
   simpl.
   split ; intros ; subst.
 
@@ -79,14 +79,14 @@ Qed.
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
    in tactics. *)
 
-Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
   fn (exist _ x eq_refl).
 
 (* This is what we want to be able to do: replace the originaly matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
 
-Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B)
-  (y : A | y = x),
+Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
+  (y : {y:A | y = x}),
   match_eq A B x fn = fn y.
 Proof.
   intros.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 269748b5..67e9a20c 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index fd55a553..0cf8d733 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index de2a76ab..e39128cb 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 2a7a5e17..d89919b0 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,6 +11,7 @@
 Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
+Require Import FunctionalExtensionality.
 
 Local Open Scope program_scope.
 
@@ -32,14 +33,13 @@ Section Well_founded.
   (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
 
-  Hypothesis
-    F_ext :
+  Hypothesis F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-      (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g.
+      (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
 
   Lemma Fix_F_eq :
     forall (x:A) (r:Acc R x),
-      F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
+      F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
   Proof.
     destruct r using Acc_inv_dep; auto.
   Qed.
@@ -50,7 +50,7 @@ Section Well_founded.
     rewrite (proof_irrelevance (Acc R x) r s) ; auto.
   Qed.
 
-  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)).
+  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
   Proof.
     intro x; unfold Fix_sub.
     rewrite <- (Fix_F_eq ).
@@ -62,7 +62,8 @@ Section Well_founded.
     forall x : A,
       Fix_sub x =
       let f_sub := F_sub in
-        f_sub x (fun (y : A | R y x) => Fix_sub (`y)).
+        f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)).
+  Proof.
     exact Fix_eq.
   Qed.
 
@@ -153,7 +154,7 @@ Section Fix_rects.
 
   Hypothesis equiv_lowers:
     forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
-    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) ->
+    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) ->
       f g = f h.
 
   (* From equiv_lowers, it follows that
@@ -221,8 +222,6 @@ Ltac fold_sub f :=
 
 Module WfExtensionality.
 
-  Require Import FunctionalExtensionality.
-
   (** The two following lemmas allow to unfold a well-founded fixpoint definition without
      restriction using the functional extensionality axiom. *)
 
@@ -231,10 +230,10 @@ Module WfExtensionality.
   Program Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
-      (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-          F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y).
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)).
   Proof.
     intros ; apply Fix_eq ; auto.
     intros.
-- 
cgit v1.2.3