15 files changed, 442 insertions, 54 deletions
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index c61d89a00f..ee3d5fe0d6 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -40,7 +40,7 @@ Proof.
   induction n.
     auto with arith.
     elim IHn; auto with arith.
-Qed.
+Defined.
 
 Lemma not_even_and_odd : forall n, even n -> odd n -> False.
 Proof.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
new file mode 100644
index 0000000000..3070053822
--- /dev/null
+++ b/theories/Classes/Init.v
@@ -0,0 +1 @@
+Instantiation Tactic := eauto 50 with typeclass_instances || eauto.
diff --git a/theories/Classes/Init.v.d b/theories/Classes/Init.v.d
new file mode 100644
index 0000000000..482ac0796e
--- /dev/null
+++ b/theories/Classes/Init.v.d
@@ -0,0 +1 @@
+theories/Classes/Init.vo theories/Classes/Init.glob: theories/Classes/Init.v
diff --git a/theories/Classes/Setoid.v b/theories/Classes/Setoid.v
new file mode 100644
index 0000000000..915a7a944a
--- /dev/null
+++ b/theories/Classes/Setoid.v
@@ -0,0 +1,192 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * 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 $ *)
+
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Init.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** We first define setoids on a carrier, it amounts to an equivalence relation. 
+   Now [equiv] is overloaded for every [Setoid].
+*)
+
+Require Export Coq.Relations.Relations.
+
+Class Setoid (carrier : Type) (equiv : relation carrier) :=
+  equiv_prf : equivalence carrier equiv.
+
+(** Overloaded notation for setoid equivalence. Not to be confused with [eq] and [=]. *)
+
+Definition equiv [ Setoid A R ] : _ := R.
+
+Infix "==" := equiv (at level 70, no associativity).
+
+Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
+Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
+Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
+
+
+Ltac refl :=
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
+    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
+    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
+    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
+    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
+  end.
+
+Ltac sym := 
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
+    | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
+  end.
+
+Ltac trans Y := 
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
+  end.
+
+Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop :=
+  forall x y, eqa x y -> eqb (m x) (m y).
+
+Class [ Setoid a eqa, Setoid b eqb ] => Morphism (m : a -> b) :=
+  respect : respectful m.
+
+(** Here we build a setoid instance for functions which relates respectful ones only. *)
+
+Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }.
+
+Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto.
+
+Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
+  Setoid ({ morph : a -> b | respectful morph })
+  (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Next Obligation.
+Proof.
+  trans (y x0) ; eauto.
+  apply H.
+  refl.
+Qed.
+
+Next Obligation.
+Proof.
+  sym ; apply H.
+  sym ; auto.
+Qed.
+
+(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
+   some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
+
+Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop :=
+  forall x y, eqa x y -> 
+    forall z w, eqb z w -> eqc (m x z) (m y w).
+
+Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) :=
+  respect2 : binary_respectful m.
+
+Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop :=
+  forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v).
+
+Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) :=
+  respect3 : ternary_respectful m.
+
+(** Definition of the usual morphisms in [Prop]. *)
+
+Program Instance iff_setoid : Setoid Prop iff :=
+  equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
+
+Program Instance not_morphism : Morphism Prop iff Prop iff not.
+
+Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
+
+(* We make the setoids implicit, they're always [iff] *)
+
+Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]].
+
+Program Instance or_morphism : ? BinaryMorphism or.
+
+Definition impl (A B : Prop) := A -> B.
+
+Program Instance impl_morphism : ? BinaryMorphism impl.
+
+Next Obligation.
+Proof.
+  unfold impl. tauto.
+Qed.
+
+(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
+
+Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R.
+
+Next Obligation.
+Proof with auto.
+  split ; intros.
+  trans x. sym... trans z...
+  trans y... trans w... sym...
+Qed.
+  
+Definition iff_morphism : BinaryMorphism iff := setoid_morphism.
+
+Existing Instance iff_morphism.
+
+Implicit Arguments eq [[A]].
+
+Program Instance eq_setoid : Setoid A eq :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq.
+
+Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m.
+
+Implicit Arguments arrow_morphism [[A] [B] [C]].
+
+Program Instance type_setoid : Setoid Type (fun x y => x = y) :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Lemma setoid_subst : forall (x y : Type), x == y -> x -> y.
+Proof.
+  intros.
+  rewrite <- H.
+  apply X.
+Qed.
+
+Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y.
+Proof.
+  intros.
+  clrewrite <- H.
+  apply H0.
+Qed.
+
+Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
+  ? Morphism sb sc g, ? Morphism sa sb f ] => 
+  compose_morphism : ? Morphism sa sc (fun x => g (f x)).
+
+Next Obligation.
+Proof.
+  apply (respect (m0:=m)).
+  apply (respect (m0:=m0)).
+  assumption.
+Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
new file mode 100644
index 0000000000..8e037db1a3
--- /dev/null
+++ b/theories/Classes/SetoidTactics.v
@@ -0,0 +1,37 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * 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 $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.Setoid.
+
+Ltac rew H := clrewrite H.
+
+Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y.
+Proof.
+  admit.
+Qed.
+
+Implicit Arguments setoideq_eq [[a] [eqa] [sa]].
+
+Ltac setoideq :=
+  match goal with
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
+  end.
+
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d0bf5bee9a..d9f5d10a1d 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -9,7 +9,7 @@
   (*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
-Require Import Setoid.
+Require Import Coq.Setoids.Setoid.
 
 Set Implicit Arguments.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 96c1c8f4d1..85ed188910 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -85,17 +85,6 @@ Ltac abstract_eq_hyp H' p :=
       end
     end.
 
-(** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *)
-
-Ltac abstract_any_hyp H' p := 
-  match type of p with
-    ?X => 
-    match goal with 
-      | [ H : X |- _ ] => fail 1
-      | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H'
-    end
-  end.
-
 (** Apply the tactic tac to proofs of equality appearing as coercion arguments. 
    Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators.
    *)
@@ -180,3 +169,39 @@ Ltac clear_eqs := repeat clear_eq.
 Ltac simplify_eqs := 
   simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ;  
     try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id.
+
+(** A tactic to remove trivial equality guards in hypotheses. *)
+
+Ltac simpl_IH_eq H :=
+  let tac H' := clear H ; rename H' into H in
+  let H' := fresh "H" in
+    match type of H with
+      | JMeq _ _ -> _ =>
+        assert (H' := H (JMeq_refl _)) ; tac H'
+      | _ = _ -> _ =>
+        assert (H' := H (refl_equal _)) ; tac H'
+    end.
+
+Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
+
+Ltac simpl_IHs_eqs := 
+  match goal with
+    | [ H : JMeq _ _ -> _ |- _ ] => simpl_IH_eqs H
+    | [ H : _ = _ -> _ |- _ ] => simpl_IH_eqs H
+  end.
+
+Require Import Coq.Program.Tactics.
+
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+   by first generalizing it and adding the proper equalities to the context, in a maner similar to 
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
+
+Tactic Notation "dependent" "induction" ident(H) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
+
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 22cb93d56b..382252ce2a 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -48,13 +48,13 @@ Ltac apply_ext :=
 
 (** For a function defined with Program using a well-founded order. *)
 
-Lemma fix_sub_eq_ext :
+Program Lemma fix_sub_eq_ext :
   forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
     (P : A -> Set)
-    (F_sub : forall x : A, (forall  {y : A | R y x}, P (`y)) -> P x),
+    (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 =
-        F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
+        F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y).
 Proof.
   intros ; apply Fix_eq ; auto.
   intros.
@@ -65,12 +65,12 @@ Qed.
 
 (** For a function defined with Program using a measure. *)
 
-Lemma fix_sub_measure_eq_ext :
+Program Lemma fix_sub_measure_eq_ext :
   forall (A : Type) (f : A -> nat) (P : A -> Type)
-    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
+    (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
     forall x : A,
       Fix_measure_sub A f P F_sub x =
-        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
+        F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
 Proof.
   intros ; apply Fix_measure_eq ; auto.
   intros.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 39c5b77341..fb172db845 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,3 +1,4 @@
 Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
+Require Export Coq.Program.Subset.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
new file mode 100644
index 0000000000..54d830c899
--- /dev/null
+++ b/theories/Program/Subset.v
@@ -0,0 +1,141 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.Program.Utils.
+Require Import Coq.Program.Equality.
+
+(** Tactics related to subsets and proof irrelevance. *)
+
+(** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
+
+Ltac simpl_existT :=
+  match goal with
+    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
+    let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
+  end.
+
+Ltac simpl_existTs := repeat simpl_existT.
+
+(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
+   factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
+
+Ltac on_subset_proof_aux tac T :=
+  match T with
+    | context [ exist ?P _ ?p ] => try on_subset_proof_aux tac P ; tac p
+  end.
+
+Ltac on_subset_proof tac :=
+  match goal with
+    [ |- ?T ] => on_subset_proof_aux tac T
+  end.
+
+Ltac abstract_any_hyp H' p := 
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => fail 1
+      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
+    end
+  end.
+
+Ltac abstract_subset_proof := 
+  on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H).
+
+Ltac abstract_subset_proofs := repeat abstract_subset_proof.
+
+Ltac pi_subset_proof_hyp p :=
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => 
+        match p with
+          | H => fail 2
+          | _ => rewrite (proof_irrelevance X p H)
+        end
+      | _ => fail " No hypothesis with same type "
+    end
+  end.
+
+Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp.
+
+Ltac pi_subset_proofs := repeat pi_subset_proof.
+
+(** Clear duplicated hypotheses *)
+
+Ltac clear_dup :=
+  match goal with 
+    | [ H : ?X |- _ ] => 
+      match goal with
+        | [ H' : X |- _ ] =>
+          match H' with
+            | H => fail 2 
+            | _ => clear H' || clear H
+          end
+      end
+  end.
+
+Ltac clear_dups := repeat clear_dup.
+
+(** The two preceding tactics in sequence. *)
+
+Ltac clear_subset_proofs :=
+  abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups.
+
+Ltac pi := repeat progress 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.
+  simpl.
+  split ; intros ; subst.
+
+  inversion H.
+  reflexivity.
+
+  pi.
+Qed.
+
+(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] 
+   in tactics. *)
+
+Program Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+  fn (exist _ x (refl_equal x)).
+
+(* 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),
+  match_eq A B x fn = fn y.
+Proof.
+  intros.
+  unfold match_eq.
+  f_equal.
+  destruct y.
+  (* uses proof-irrelevance *)
+  apply <- subset_eq.
+  symmetry. assumption.
+Qed.
+
+(** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary
+   equality [t = u], and [u] is now the subject of the [match]. *)
+
+Ltac rewrite_match_eq H := 
+  match goal with
+    [ |- ?T ] => 
+    match T with
+      context [ match_eq ?A ?B ?t ?f ] =>
+      rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H)))
+    end
+  end.
+
+(** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *)
+
+Ltac simpl_match_eq := unfold match_eq ; simpl.
+
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index e4c60e14af..ac0f5cf717 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -50,6 +50,7 @@ Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
 Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
 
 (** Discriminate that also work on a [x <> x] hypothesis. *)
+
 Ltac discriminates :=
   match goal with
     | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
@@ -151,21 +152,12 @@ Ltac bang :=
 Tactic Notation "contradiction" "by" constr(t) := 
   let H := fresh in assert t as H by auto with * ; contradiction.
 
-(** The following tactics allow to do induction on an already instantiated inductive predicate
-   by first generalizing it and adding the proper equalities to the context, in a manner similar to 
-   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
-
-Tactic Notation "dependent" "induction" ident(H) := 
-  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    induction H ; intros ; subst* ; try discriminates.
-
-(** This tactic also generalizes the goal by the given variables before the induction. *)
-
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
-  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates.
+(** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *]
+   is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, 
+   possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
-(** The default simplification tactic used by Program. *)
+Ltac program_simplify :=
+  simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; 
+    try (solve [ red ; intros ; destruct_conjs ; discriminate ]).
 
-Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; destruct_conjs ; discriminate ]) ; auto with *.  
+Ltac program_simpl := program_simplify ; auto with *.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index a268f0afb5..6af81a4105 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -18,9 +18,9 @@ Notation " {{ x }} " := (tt : { y : unit | x }).
 
 (** A simpler notation for subsets defined on a cartesian product. *)
 
-Notation "{ ( x , y )  :  A  |  P }" := 
-  (sig (fun anonymous : A => let (x,y) := anonymous in P))
-  (x ident, y ident) : type_scope.
+(* Notation "{ ( x , y )  :  A  |  P }" :=  *)
+(*   (sig (fun anonymous : A => let (x,y) := anonymous in P)) *)
+(*   (x ident, y ident, at level 10) : type_scope. *)
 
 (** Generates an obligation to prove False. *)
 
@@ -45,13 +45,13 @@ Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
 (** Quantifying over subsets. *)
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
+(* Notation "'fun' ( x : A | P ) => Q" := *)
+(*   (fun (x :A|P} => Q) *)
+(*   (at level 200, x ident, right associativity). *)
 
-Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, Q)
-  (at level 200, x ident, right associativity).
+(* Notation "'forall' ( x : A | P ), Q" := *)
+(*   (forall (x : A | P), Q) *)
+(*   (at level 200, x ident, right associativity). *)
 
 Require Import Coq.Bool.Sumbool.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 55784671f5..70b1b1b5a2 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -34,11 +34,11 @@ Section Well_founded.
     Hypothesis
       F_ext :
       forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-        (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
+        (forall (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:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
     Proof. 
       destruct r using Acc_inv_dep; auto.
     Qed.
@@ -52,7 +52,7 @@ Section Well_founded.
       rewrite (proof_irrelevance (Acc R x) r s) ; auto.
     Qed.
 
-    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
+    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)).
     Proof.
       intro x; unfold Fix in |- *.
       rewrite <- (Fix_F_eq ).
@@ -64,7 +64,7 @@ Section Well_founded.
         forall x : A,
           Fix_sub P F_sub x =
           let f_sub := F_sub in
-            f_sub x (fun  {y : A | R y x}=> Fix (`y)).
+            f_sub x (fun (y : A | R y x) => Fix (`y)).
       exact Fix_eq.
     Qed.
 
@@ -98,7 +98,7 @@ Section Well_founded_measure.
   Section FixPoint.
     Variable P : A -> Type.
     
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x.
     
     Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
     
@@ -106,8 +106,8 @@ Section Well_founded_measure.
     
     Hypothesis
       F_ext :
-      forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)),
-        (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
+      forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
+        (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
 
     Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
@@ -137,7 +137,7 @@ Section Well_founded_measure.
         forall x : A,
           Fix_measure_sub P F_sub x =
           let f_sub := F_sub in
-            f_sub x (fun  {y : A | m y < m x}=> Fix_measure (`y)).
+            f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
       exact Fix_measure_eq.
     Qed.
 
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 18e8b6e77e..f93a12955c 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/Setoids/Setoid_tac.v b/theories/Setoids/Setoid_tac.v
index f979ec11c4..664316805e 100644
--- a/theories/Setoids/Setoid_tac.v
+++ b/theories/Setoids/Setoid_tac.v
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)