Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

16 files changed, 73 insertions, 89 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 157217ae..15cabf81 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,9 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Export notations. *)
 
@@ -144,9 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
 
-  Next Obligation.
-  Proof. clear aux. red in H0. subst. 
-    destruct y; intuition (discriminate || eauto).
-  Defined.
+  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5e5895ab..7068bc6b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,15 +12,15 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud
    91405 Orsay, France *) 
 
-(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 5df7a4ed..762cc5c1 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,12 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
-
-Tactic Notation "clapply" ident(c) :=
-  eapply @c ; typeclasses eauto.
+(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
@@ -29,12 +24,12 @@ Typeclasses Opaque id const flip compose arrow impl iff.
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
-Class Unconvertible (A : Type) (a b : A).
+Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
 
 Ltac unconvertible :=
   match goal with
     | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
-    | |- _ => eapply Build_Unconvertible 
+    | |- _ => exact tt
   end.
 
 Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 86097a56..2b653e27 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,9 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -55,18 +52,24 @@ Definition respectful {A B : Type}
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+
 Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
-  (right associativity, at level 55) : signature_scope.
+Module MorphismNotations.
 
-Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
 
-Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+End MorphismNotations.
 
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Export MorphismNotations.
 
 Open Local Scope signature_scope.
 
@@ -118,7 +121,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Instance morphisms_subrelation_refl : ! subrelation A R R.
 Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -151,10 +154,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Instance iff_impl_subrelation : subrelation iff impl.
+Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
 Proof. firstorder. Qed.
 
 Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
@@ -372,25 +375,6 @@ Ltac partial_application_tactic :=
       end
   end.
 
-Section PartialAppTest.
-  Instance and_ar : Params and 0.
-
-  Goal Morphism (iff) (and True True).
-    partial_application_tactic.
-  Admitted.
-
-  Goal Morphism (iff) (or True True).
-    partial_application_tactic.
-    partial_application_tactic. 
-  Admitted.
-
-  Goal Morphism (iff ==> iff) (iff True).
-    partial_application_tactic.
-    (*partial_application_tactic. *)
-   Admitted.
-
-End PartialAppTest.
-
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 24b8d636..4654e654 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -12,6 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
    91405 Orsay, France *)
 
+Require Import Relation_Definitions.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Program.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f95894be..e1de9ee9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -13,12 +13,12 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 
 (** We allow to unfold the [relation] definition while doing morphism search. *)
 
@@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
@@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal. 
+  pose proof partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
 Qed.
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 305168ec..03bb9a80 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
 
 Require Import Coq.Program.Program.
 
@@ -22,7 +22,7 @@ Unset Strict Implicit.
 Require Export Coq.Classes.SetoidClass.
 
 (* Application of the extensionality axiom to turn a goal on 
-   Leibinz equality to a setoid equivalence (use with care!). *)
+   Leibniz equality to a setoid equivalence (use with care!). *)
 
 Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 47f92ada..d3da7d5a 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,14 +12,14 @@
    Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Import Coq.Program.Program.
 
-Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Import Coq.Classes.Functions.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index caacc9ec..36f05e31 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,13 +13,13 @@
  * Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+
+Export MorphismNotations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index df12166e..d91eb87a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FMapFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** * Finite maps library *)
 
@@ -15,7 +15,7 @@
   different styles: equivalence and boolean equalities. 
 *)
 
-Require Import Bool DecidableType DecidableTypeEx OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
 Require Export FMapInterface. 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 1e15d3a1..674caaac 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FSetFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** * Finite sets library *)
 
@@ -17,7 +17,7 @@
 *)
 
 Require Import DecidableTypeEx.
-Require Export FSetInterface. 
+Require Export FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -424,14 +424,14 @@ Add Relation t Subset
  transitivity proved by Subset_trans
  as SubsetSetoid.
 
-Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
+Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1.
 Proof.
   simpl_relation. eauto with set.
 Qed.
 
-Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.
 Proof.
-unfold Subset, Empty, impl; firstorder.
+unfold Subset, Empty, Basics.impl; firstorder.
 Qed.
 
 Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 3753b97b..ff70c9fb 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
 
 (** This module proves the constructive description schema, which
 infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -14,8 +14,8 @@ predicate from the regular existence (i.e., [Prop]-existence). One
 requires that the underlying set is countable and that the predicate
 is decidable. *)
 
-(** Coq does not allow case analysis on sort [Set] when the goal is in
-[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+(** Coq does not allow case analysis on sort [Prop] when the goal is in
+[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
 show [{n : nat | P n}]. However, one can perform a recursion on an
 inductive predicate in sort [Prop] so that the returning type of the
 recursion is in [Set]. This trick is described in Coq'Art book, Sect.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 4445b0e1..0dc82907 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -11,8 +11,6 @@
 (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
    It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
 
-Set Manual Implicit Arguments.
-
 (** The converse of functional extensionality. *)
 
 Lemma equal_f : forall {A B : Type} {f g : A -> B}, 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 99d54755..9681d543 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
+(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -479,8 +479,12 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
-Ltac do_ind p := induction p || elim_ind p.
+Ltac introduce p := 
+  first [ match p with _ => idtac end (* Already there *)
+    | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
 Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 12bdf3a7..2083e530 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)
@@ -165,7 +165,7 @@ Section Measure_well_founded.
 
   (* Measure relations are well-founded if the underlying relation is well-founded. *)
 
-  Variables T M: Set.
+  Variables T M: Type.
   Variable R: M -> M -> Prop.
   Hypothesis wf: well_founded R.
   Variable m: T -> M.
@@ -191,7 +191,7 @@ End Measure_well_founded.
 
 Section Fix_measure_rects.
 
-  Variable A: Set.
+  Variable A: Type.
   Variable m: A -> nat.
   Variable P: A -> Type.
   Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
@@ -287,7 +287,7 @@ Section Fix_measure_rects.
 
 End Fix_measure_rects.
 
-(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
+(** Tactic to fold a definition based on [Fix_measure_sub]. *)
 
 Ltac fold_sub f :=
   match goal with
@@ -312,8 +312,8 @@ Module WfExtensionality.
   (** For a function defined with Program using a well-founded order. *)
 
   Program Lemma fix_sub_eq_ext :
-    forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
-      (P : A -> Set)
+    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),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index e7fe82b2..a187a7c6 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -6,10 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Setoid.v 11720 2008-12-28 07:12:15Z letouzey $: i*)
+(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*)
 
 Require Export Coq.Classes.SetoidTactics.
 
+Export Morphisms.MorphismNotations.
+
 (** For backward compatibility *)
 
 Definition Setoid_Theory := @Equivalence.