Reorganize Program and Classes theories. Requiring Setoid no longer sets

implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 204 insertions, 164 deletions

diff --git a/Makefile.common b/Makefile.common
index 6fe218863..44271647e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -748,7 +748,7 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
+CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \
 	theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
 	theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo
 
@@ -806,8 +806,9 @@ CCVO:=
 DPVO:=contrib/dp/Dp.vo
 
 SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \
-	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \
-	theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo
+	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Basics.vo \
+	theories/Program/FunctionalExtensionality.vo theories/Program/Combinators.vo \
+	theories/Program/Syntax.vo theories/Program/Program.vo 
 
 RTAUTOVO:= \
  contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo
diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v
index d410606a7..cd0f1afe9 100644
--- a/contrib/rtauto/Bintree.v
+++ b/contrib/rtauto/Bintree.v
@@ -107,7 +107,7 @@ intro ne;right;congruence.
 left;reflexivity.
 Defined.
 
-Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m).
+Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m).
 fix 1;intros [mm|mm|].
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
@@ -116,7 +116,7 @@ Qed.
 
 Theorem pos_eq_dec_ex : forall m n,
  pos_eq m n =true -> exists h:m=n,
- pos_eq_dec m n = left h.
+ pos_eq_dec m n = left _ h.
 fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8f11989a1..71ab3a5f7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -360,28 +360,25 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
 let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
 
-let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive")
-let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive")
+let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive")
+let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive")
 
-let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric")
-let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric")
+let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric")
+let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric")
 
-let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive")
-let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive")
+let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive")
+let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
 
-let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse")
+let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
 
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
-let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence")
-let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation")
+let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence")
+let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation")
 
-let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
-let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
-
-(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+(* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *)
+let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
 let coq_relation a = mkApp (Lazy.force coq_relation, [| a |])
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index a19f8da82..052d21019 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -8,7 +8,6 @@
 (************************************************************************)
 
 (* Typeclass-based setoids, tactics and standard instances.
-   TODO: explain clrewrite, clsubstitute and so on.
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
@@ -17,10 +16,10 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Export Coq.Program.Basics.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Classes.SetoidTactics.
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index c08dee76f..11c60a3aa 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -16,7 +16,7 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Import Coq.Program.Program.
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 37190ac75..eaf300fd2 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -15,8 +15,9 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
-Require Export Coq.Classes.Relations.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Classes.RelationClasses.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -53,6 +54,7 @@ Class Morphism A (R : relation A) (m : A) :=
 Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
   { morph : A -> B | respectful R R' morph morph }.
 
+
 Ltac obligations_tactic ::= program_simpl.
 
 Program Instance [ Equivalence A R, Equivalence B R' ] => 
@@ -180,8 +182,6 @@ Hint Resolve @subrelation_morphism 4 : typeclass_instances.
 
 (* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *)
 
-
-
 (* Program Instance `A` (R : relation A) `B` (R' : relation B) *)
 (*   [ ? Morphism (R ==> R' ==> iff) m ] => *)
 (*   iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *)
@@ -381,7 +381,7 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B)
    to get an [R y z] goal. *)
 
 Program Instance [ ! Transitive A R ] => 
-  trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R.
+  trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -390,7 +390,7 @@ Program Instance [ ! Transitive A R ] =>
   Qed.
 
 Program Instance [ ! Transitive A R ] => 
-  trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R.
+  trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
   Proof with auto.
diff --git a/theories/Classes/Relations.v b/theories/Classes/RelationClasses.v
index 326e97a41..659f9528c 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/RelationClasses.v
@@ -17,15 +17,13 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Relations.Relation_Definitions.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* Notation "'relation' A " := (A -> A -> Prop) (at level 0). *)
-
-Definition relation A := A -> A -> Prop.
-
 (** Default relation on a given support. *)
 
 Class DefaultRelation A (R : relation A).
@@ -35,14 +33,12 @@ Class DefaultRelation A (R : relation A).
 Definition default_relation [ DefaultRelation A R ] : relation A := R.
 
 (** A notation for applying the default relation to [x] and [y]. *)
-Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
 
-Definition inverse A (R : relation A) : relation A := fun x y => R y x.
+Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
 
-Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
-Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
+Definition inverse {A} : relation A -> relation A := flip.
 
-Definition complement A (R : relation A) : relation A := fun x y => R x y -> False.
+Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
@@ -355,7 +351,7 @@ Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] =
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
-Program Instance eq_equivalence : Equivalence A eq.
+Program Instance eq_equivalence : Equivalence A (@eq A).
 
 (** Logical equivalence [iff] is an equivalence relation. *)
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 9dd4f6181..86e9078e9 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -22,7 +22,7 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Classes.Functions.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index c71db6995..9f6dfab42 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,7 +15,7 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 832829135..6d77a6a0c 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -675,7 +675,7 @@ rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
 Add Morphism (@MapsTo elt)
- with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m.
+ with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
 rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
@@ -689,19 +689,19 @@ rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m.
+Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m.
+Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m.
+Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
 Proof.
 intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
@@ -713,7 +713,7 @@ symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
 Add Morphism (@add elt) with signature 
- E.eq ==> Logic.eq ==> Equal ==> Equal as add_m.
+ E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
@@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m.
+Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m.
+ Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 27d9c72bd..fc2cc81eb 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
+Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index ddc61a2dc..d6c276d16 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,133 +6,50 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Standard functions and proofs about them.
+(* Standard functions and combinators.
+ * Proofs about them require functional extensionality and can be found in [Combinators].
+ *
  * Author: Matthieu Sozeau
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Set Implicit Arguments.
-Unset Strict Implicit.
+(** The polymorphic identity function. *)
 
-Require Export Coq.Program.FunctionalExtensionality.
+Definition id {A} := fun x : A => x.
 
-Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
+(** Function composition. *)
 
-Open Local Scope program_scope.
-
-Definition id {A} := λ x : A, x.
-
-Definition compose {A B C} (g : B -> C) (f : A -> B) := λ x : A , g (f x).
+Definition compose {A B C} (f : A -> B) (g : B -> C) := fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose g f)  (at level 50, left associativity) : program_scope.
-
-Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f.
-Proof.
-  intros.
-  unfold id, compose.
-  symmetry ; apply eta_expansion.
-Qed.
+Notation " g ∘ f " := (compose f g)  (at level 50, left associativity) : program_scope.
 
-Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f.
-Proof.
-  intros.
-  unfold id, compose.
-  symmetry ; apply eta_expansion.
-Qed.
-
-Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
-  h ∘ g ∘ f = h ∘ (g ∘ f).
-Proof.
-  intros.
-  reflexivity.
-Qed.
+Open Local Scope program_scope.
 
-Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core.
+(** [arrow A B] represents the non-dependent function space between [A] and [B]. *)
 
 Definition arrow (A B : Type) := A -> B.
 
+(** [impl A B] represents the logical implication of [B] by [A]. *)
+
 Definition impl (A B : Prop) : Prop := A -> B.
 
-(* Notation " f  x " := (f x) (at level 100, x at level 200, only parsing) : program_scope. *)
+(** The constant function [const a] always returns [a]. *)
 
-Definition const {A B} (a : A) := fun x : B => a.
+Definition const {A B} (a : A) := fun _ : B => a.
+
+(** The [flip] combinator reverses the first two arguments of a function. *)
 
 Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
-Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f.
-Proof.
-  unfold flip.
-  intros.
-  extensionality x ; extensionality y.
-  reflexivity.
-Qed.
+(** [apply f x] simply applies [f] to [x]. *)
 
 Definition apply {A B} (f : A -> B) (x : A) := f x.
 
-(** Notations for the unit type and value. *)
-
-Notation " () " := Datatypes.unit : type_scope.
-Notation " () " := tt.
-
-(** Set maximally inserted implicit arguments for standard definitions. *)
-
-Implicit Arguments eq [[A]].
-
-Implicit Arguments Some [[A]].
-Implicit Arguments None [[A]].
-
-Implicit Arguments inl [[A] [B]].
-Implicit Arguments inr [[A] [B]].
-
-Implicit Arguments left [[A] [B]].
-Implicit Arguments right [[A] [B]].
-
-(** Curryfication. *)
-
-Definition curry {a b c} (f : a -> b -> c) (p : prod a b) : c :=
-  let (x, y) := p in f x y.
-
-Definition uncurry {a b c} (f : prod a b -> c) (x : a) (y : b) : c :=
-  f (x, y).
-
-Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f.
-Proof.
-  simpl ; intros.
-  unfold uncurry, curry.
-  extensionality x ; extensionality y.
-  reflexivity.
-Qed.
-
-Lemma curry_uncurry : forall a b c (f : prod a b -> c), curry (uncurry f) = f.
-Proof.
-  simpl ; intros.
-  unfold uncurry, curry.
-  extensionality x. 
-  destruct x ; simpl ; reflexivity.
-Qed.
-
-(** n-ary exists ! *)
-
-Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
-  (at level 200, x ident, y ident, right associativity) : type_scope.
-
-Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
-  (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
-
-Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
-  (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
-
-Tactic Notation "exist" constr(x) := exists x.
-Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
-
-(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
-(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
+(** Curryfication of [prod] is defined in [Logic.Datatypes]. *)
 
-(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
-(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
+Implicit Arguments prod_curry [[A] [B] [C]].
+Implicit Arguments prod_uncurry [[A] [B] [C]].
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
new file mode 100644
index 000000000..e267fbbe2
--- /dev/null
+++ b/theories/Program/Combinators.v
@@ -0,0 +1,71 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Proofs about standard combinators, exports functional extensionality.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+Require Import Coq.Program.Basics.
+Require Export Coq.Program.FunctionalExtensionality.
+
+Open Scope program_scope.
+
+(** Composition has [id] for neutral element and is associative. *)
+
+Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f.
+Proof.
+  intros.
+  unfold id, compose.
+  symmetry. apply eta_expansion.
+Qed.
+
+Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f.
+Proof.
+  intros.
+  unfold id, compose.
+  symmetry ; apply eta_expansion.
+Qed.
+
+Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
+  h ∘ g ∘ f = h ∘ (g ∘ f).
+Proof.
+  intros.
+  reflexivity.
+Qed.
+
+Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core.
+
+(** [flip] is involutive. *)
+
+Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id.
+Proof.
+  unfold flip, compose.
+  intros.
+  extensionality x ; extensionality y ; extensionality z.
+  reflexivity.
+Qed.
+
+(** [prod_curry] and [prod_uncurry] are each others inverses. *)
+
+Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id.
+Proof.
+  simpl ; intros.
+  unfold prod_uncurry, prod_curry, compose.
+  extensionality x ; extensionality y ; extensionality z.
+  reflexivity.
+Qed.
+
+Lemma prod_curry_uncurry : forall A B C, @prod_curry A B C ∘ prod_uncurry = id.
+Proof.
+  simpl ; intros.
+  unfold prod_uncurry, prod_curry, compose.
+  extensionality x ; extensionality p.
+  destruct p ; simpl ; reflexivity.
+Qed.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 4d92be3c5..b6c3031e7 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -2,4 +2,6 @@ Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
 Require Export Coq.Program.Subset.
-Require Export Coq.Program.Basics.
\ No newline at end of file
+Require Export Coq.Program.Basics.
+Require Export Coq.Program.Combinators.
+Require Export Coq.Program.Syntax.
\ No newline at end of file
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
new file mode 100644
index 000000000..ecdacce64
--- /dev/null
+++ b/theories/Program/Syntax.v
@@ -0,0 +1,58 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Custom notations and implicits for Coq prelude definitions.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(** Unicode lambda abstraction, does not work with factorization of lambdas. *)
+
+Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
+
+(** Notations for the unit type and value. *)
+
+Notation " () " := Datatypes.unit : type_scope.
+Notation " () " := tt.
+
+(** Set maximally inserted implicit arguments for standard definitions. *)
+
+Implicit Arguments eq [[A]].
+
+Implicit Arguments Some [[A]].
+Implicit Arguments None [[A]].
+
+Implicit Arguments inl [[A] [B]].
+Implicit Arguments inr [[A] [B]].
+
+Implicit Arguments left [[A] [B]].
+Implicit Arguments right [[A] [B]].
+
+(** n-ary exists ! *)
+
+Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
+  (at level 200, x ident, y ident, right associativity) : type_scope.
+
+Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
+  (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
+
+Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
+  (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
+
+Tactic Notation "exist" constr(x) := exists x.
+Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
+Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
+Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
+(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
+
+(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
+(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index cde670075..26638893a 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -775,7 +775,7 @@ Qed.
 Definition Qpower_positive (q:Q)(p:positive) : Q := 
  pow_pos Qmult q p.
 
-Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp.
+Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp.
 Proof.
 intros x1 x2 Hx y.
 unfold Qpower_positive.
@@ -794,7 +794,7 @@ Definition Qpower (q:Q) (z:Z) :=
 
 Notation " q ^ z " := (Qpower q z) : Q_scope.
 
-Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp.
+Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp.
 Proof.
 intros x1 x2 Hx [|y|y]; try reflexivity;
 simpl; rewrite Hx; reflexivity.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 8162a702f..3f191c752 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -122,7 +122,7 @@ Qed.
 
 Hint Resolve Qceiling_resp_le : qarith.
 
-Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
+Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.
@@ -130,7 +130,7 @@ apply Zle_antisym.
 symmetry in H; auto with *.
 Qed.
 
-Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.
+Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 61b70ba68..a5ad269d4 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
 Inductive le_AsB : A + B -> A + B -> Prop :=
-  | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y)
-  | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y)
-  | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y).
+  | le_aa : forall x y:A, leA x y -> le_AsB (inl _ x) (inl _ y)
+  | le_ab : forall (x:A) (y:B), le_AsB (inl _ x) (inr _ y)
+  | le_bb : forall x y:B, leB x y -> le_AsB (inr _ x) (inr _ y).
 
 End Disjoint_Union. 
 
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index a86d19c09..f6ce84f98 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -21,7 +21,7 @@ Section Wf_Disjoint_Union.
 
   Notation Le_AsB := (le_AsB A B leA leB).
   
-  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x).
+  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
   Proof.
     induction 1.
     apply Acc_intro; intros y H2.
@@ -30,7 +30,7 @@ Section Wf_Disjoint_Union.
   Qed.
 
   Lemma acc_B_sum :
-    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x).
+    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
   Proof.
     induction 2.
     apply Acc_intro; intros y H3.