Imported Upstream snapshot 8.3~beta0+13298

10 files changed, 284 insertions, 99 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 0163c01c..6040f58b 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,12 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Datatypes.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
+Declare ML Module "nat_syntax_plugin".
+
 
 (** [unit] is a singleton datatype with sole inhabitant [tt] *)
 
@@ -72,6 +74,16 @@ Hint Resolve andb_true_intro: bool.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+Hint Constructors eq_true : eq_true.
+
+(** Another way of interpreting booleans as propositions *)
+
+Definition is_true b := b = true.
+
+(** [is_true] can be activated as a coercion by
+   (Local) Coercion is_true : bool >-> Prop.
+*)
+
 (** Additional rewriting lemmas about [eq_true] *)
 
 Lemma eq_true_ind_r :
@@ -94,7 +106,7 @@ Defined.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
-    Numbers in [nat] can be denoted using a decimal notation; 
+    Numbers in [nat] can be denoted using a decimal notation;
     e.g. [3%nat] abbreviates [S (S (S O))] *)
 
 Inductive nat : Set :=
@@ -114,8 +126,8 @@ Inductive Empty_set : Set :=.
     sole inhabitant is denoted [refl_identity A a] *)
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
-  refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core.
+  identity_refl : identity a a.
+Hint Resolve identity_refl: core.
 
 Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
@@ -162,7 +174,7 @@ Section projections.
   Definition snd (p:A * B) := match p with
 				| (x, y) => y
                               end.
-End projections. 
+End projections.
 
 Hint Resolve pair inl inr: core.
 
@@ -177,13 +189,13 @@ Lemma injective_projections :
     fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
   destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
-  rewrite Hfst; rewrite Hsnd; reflexivity. 
+  rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Definition prod_uncurry (A B C:Type) (f:prod A B -> C) 
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
   (x:A) (y:B) : C := f (pair x y).
 
-Definition prod_curry (A B C:Type) (f:A -> B -> C) 
+Definition prod_curry (A B C:Type) (f:A -> B -> C)
   (p:prod A B) : C := match p with
                        | pair x y => f x y
                        end.
@@ -202,11 +214,84 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
+Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
+Proof.
+  destruct c; reflexivity.
+Qed.
+
+Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
+Proof.
+  destruct c; destruct c'; auto; discriminate.
+Qed.
+
+Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.
+Proof.
+  split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
+Qed.
+
+(** The [CompSpec] inductive will be used to relate a [compare] function
+    (returning a comparison answer) and some equality and order predicates.
+    Interest: [CompSpec] behave nicely with [case] and [destruct]. *)
+
+Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
+ | CompEq : eq x y -> CompSpec eq lt x y Eq
+ | CompLt : lt x y -> CompSpec eq lt x y Lt
+ | CompGt : lt y x -> CompSpec eq lt x y Gt.
+Hint Constructors CompSpec.
+
+(** For having clean interfaces after extraction, [CompSpec] is declared
+    in Prop. For some situations, it is nonetheless useful to have a
+    version in Type. Interestingly, these two versions are equivalent.
+*)
+
+Inductive CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
+ | CompEqT : eq x y -> CompSpecT eq lt x y Eq
+ | CompLtT : lt x y -> CompSpecT eq lt x y Lt
+ | CompGtT : lt y x -> CompSpecT eq lt x y Gt.
+Hint Constructors CompSpecT.
+
+Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
+ CompSpec eq lt x y c -> CompSpecT eq lt x y c.
+Proof.
+ destruct c; intros H; constructor; inversion_clear H; auto.
+Defined.
+
 (** Identity *)
 
 Definition ID := forall A:Type, A -> A.
 Definition id : ID := fun A x => x.
 
+(** Polymorphic lists and some operations *)
+
+Inductive list (A : Type) : Type :=
+ | nil : list A
+ | cons : A -> list A -> list A.
+
+Implicit Arguments nil [A].
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+Delimit Scope list_scope with list.
+Bind Scope list_scope with list.
+
+Local Open Scope list_scope.
+
+Definition length (A : Type) : list A -> nat :=
+  fix length l :=
+  match l with
+   | nil => O
+   | _ :: l' => S (length l')
+  end.
+
+(** Concatenation of two lists *)
+
+Definition app (A : Type) : list A -> list A -> list A :=
+  fix app l m :=
+  match l with
+   | nil => m
+   | a :: l1 => a :: app l1 m
+  end.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
 (* begin hide *)
 
 (* Compatibility *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ae79744f..4fca1d1d 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
@@ -112,6 +112,16 @@ Proof.
 intros; tauto.
 Qed.
 
+Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C.
+Proof.
+intros; tauto.
+Qed.
+
 Theorem or_cancel_l : forall A B C : Prop,
   (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
 Proof.
@@ -124,6 +134,16 @@ Proof.
 intros; tauto.
 Qed.
 
+Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
+Proof.
+intros; tauto.
+Qed.
+
 (** Backward direction of the equivalences above does not need assumptions *)
 
 Theorem and_iff_compat_l : forall A B C : Prop,
@@ -243,7 +263,7 @@ End universal_quantification.
     [A] which is true of [x] is also true of [y] *)
 
 Inductive eq (A:Type) (x:A) : A -> Prop :=
-    refl_equal : x = x :>A
+    eq_refl : x = x :>A
 
 where "x = y :> A" := (@eq A x y) : type_scope.
 
@@ -251,11 +271,13 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
+Implicit Arguments eq [ [A] ].
+
 Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
 
-Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve I conj or_introl or_intror eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
@@ -271,17 +293,17 @@ Section Logic_lemmas.
     Variable f : A -> B.
     Variables x y z : A.
 
-    Theorem sym_eq : x = y -> y = x.
+    Theorem eq_sym : x = y -> y = x.
     Proof.
       destruct 1; trivial.
     Defined.
-    Opaque sym_eq.
+    Opaque eq_sym.
 
-    Theorem trans_eq : x = y -> y = z -> x = z.
+    Theorem eq_trans : x = y -> y = z -> x = z.
     Proof.
       destruct 2; trivial.
     Defined.
-    Opaque trans_eq.
+    Opaque eq_trans.
 
     Theorem f_equal : x = y -> f x = f y.
     Proof.
@@ -289,30 +311,26 @@ Section Logic_lemmas.
     Defined.
     Opaque f_equal.
 
-    Theorem sym_not_eq : x <> y -> y <> x.
+    Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
       red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
     Qed.
 
-    Definition sym_equal := sym_eq.
-    Definition sym_not_equal := sym_not_eq.
-    Definition trans_equal := trans_eq.
-
   End equality.
 
   Definition eq_ind_r :
     forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rect_r :
     forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 End Logic_lemmas.
 
@@ -349,7 +367,18 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Hint Immediate sym_eq sym_not_eq: core.
+(* Aliases *)
+
+Notation sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := not_eq_sym (only parsing).
+
+Notation refl_equal := eq_refl (only parsing).
+Notation sym_equal := eq_sym (only parsing).
+Notation trans_equal := eq_trans (only parsing).
+Notation sym_not_equal := not_eq_sym (only parsing).
+
+Hint Immediate eq_sym not_eq_sym: core.
 
 (** Basic definitions about relations and properties *)
 
@@ -411,7 +440,7 @@ intros A x y z H1 H2. rewrite <- H2; exact H1.
 Qed.
 
 Declare Left Step eq_stepl.
-Declare Right Step trans_eq.
+Declare Right Step eq_trans.
 
 Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
 Proof.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index c4e5f6c7..1333f354 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic_Type.v 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** This module defines type constructors for types in [Type]
     ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
@@ -28,23 +28,23 @@ Section identity_is_a_congruence.
  Variable f : A -> B.
 
  Variables x y z : A.
- 
- Lemma sym_id : identity x y -> identity y x.
+
+ Lemma identity_sym : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma trans_id : identity x y -> identity y z -> identity x z.
+ Lemma identity_trans : identity x y -> identity y z -> identity x z.
  Proof.
   destruct 2; trivial.
  Defined.
 
- Lemma congr_id : identity x y -> identity (f x) (f y).
+ Lemma identity_congr : identity x y -> identity (f x) (f y).
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
+ Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
  Proof.
   red in |- *; intros H H'; apply H; destruct H'; trivial.
  Qed.
@@ -53,17 +53,22 @@ End identity_is_a_congruence.
 
 Definition identity_ind_r :
   forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rec_r :
   forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rect_r :
   forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
-Hint Immediate sym_id sym_not_id: core v62.
+Hint Immediate identity_sym not_identity_sym: core v62.
+
+Notation refl_id := identity_refl (only parsing).
+Notation sym_id := identity_sym (only parsing).
+Notation trans_id := identity_trans (only parsing).
+Notation sym_not_id := not_identity_sym (only parsing).
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 5f18edcd..0c628298 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Notations.v 12271 2009-08-11 10:29:45Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 43b1f634..12a8f7a4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** The type [nat] of Peano natural numbers (built from [O] and [S])
     is defined in [Datatypes.v] *)
@@ -77,8 +77,7 @@ Definition IsSucc (n:nat) : Prop :=
 
 Theorem O_S : forall n:nat, 0 <> S n.
 Proof.
-  unfold not; intros n H.
-  inversion H.
+  discriminate.
 Qed.
 Hint Resolve O_S: core.
 
@@ -90,7 +89,7 @@ Hint Resolve n_Sn: core.
 
 (** Addition *)
 
-Fixpoint plus (n m:nat) {struct n} : nat :=
+Fixpoint plus (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
@@ -130,7 +129,7 @@ Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
 
 (** Multiplication *)
 
-Fixpoint mult (n m:nat) {struct n} : nat :=
+Fixpoint mult (n m:nat) : nat :=
   match n with
   | O => 0
   | S p => m + p * m
@@ -161,7 +160,7 @@ Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
 
 (** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
-Fixpoint minus (n m:nat) {struct n} : nat :=
+Fixpoint minus (n m:nat) : nat :=
   match n, m with
   | O, _ => n
   | S k, O => n
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6492c948..685c7247 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Prelude.v 10064 2007-08-08 15:32:36Z msozeau $ i*)
+(*i $Id$ i*)
 
 Require Export Notations.
 Require Export Logic.
@@ -15,3 +15,12 @@ Require Export Specif.
 Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
+(* Initially available plugins
+   (+ nat_syntax_plugin loaded in Datatypes) *)
+Declare ML Module "extraction_plugin".
+Declare ML Module "cc_plugin".
+Declare ML Module "ground_plugin".
+Declare ML Module "dp_plugin".
+Declare ML Module "recdef_plugin".
+Declare ML Module "subtac_plugin".
+Declare ML Module "xml_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index c0f5c42a..7141f26c 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Specif.v 10923 2008-05-12 18:25:06Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Basic specifications : sets that may contain logical information *)
 
@@ -18,9 +18,9 @@ Require Import Logic.
 
 (** Subsets and Sigma-types *)
 
-(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset 
+(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset
     of elements of the type [A] which satisfy the predicate [P].
-    Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset 
+    Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
     of elements of the type [A] which satisfy both [P] and [Q]. *)
 
 Inductive sig (A:Type) (P:A -> Prop) : Type :=
@@ -29,7 +29,7 @@ Inductive sig (A:Type) (P:A -> Prop) : Type :=
 Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
-(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. 
+(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
     Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
@@ -123,7 +123,7 @@ Coercion sig_of_sigT : sigT >-> sig.
 
 Inductive sumbool (A B:Prop) : Set :=
   | left : A -> {A} + {B}
-  | right : B -> {A} + {B} 
+  | right : B -> {A} + {B}
  where "{ A } + { B }" := (sumbool A B) : type_scope.
 
 Add Printing If sumbool.
@@ -133,7 +133,7 @@ Add Printing If sumbool.
 
 Inductive sumor (A:Type) (B:Prop) : Type :=
   | inleft : A -> A + {B}
-  | inright : B -> A + {B} 
+  | inright : B -> A + {B}
  where "A + { B }" := (sumor A B) : type_scope.
 
 Add Printing If sumor.
@@ -148,50 +148,57 @@ Section Choice_lemmas.
   Variables R1 R2 : S -> Prop.
 
   Lemma Choice :
-   (forall x:S, sig (fun y:S' => R x y)) ->
-   sig (fun f:S -> S' => forall z:S, R z (f z)).
+   (forall x:S, {y:S' | R x y}) -> {f:S -> S' | forall z:S, R z (f z)}.
   Proof.
    intro H.
-   exists (fun z:S => match H z with
-                      | exist y _ => y
-                      end).
+   exists (fun z => proj1_sig (H z)).
    intro z; destruct (H z); trivial.
   Qed.
 
   Lemma Choice2 :
-   (forall x:S, sigT (fun y:S' => R' x y)) ->
-   sigT (fun f:S -> S' => forall z:S, R' z (f z)).
+   (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}.
   Proof.
     intro H.
-    exists (fun z:S => match H z with
-                       | existT y _ => y
-                       end).
+    exists (fun z => projT1 (H z)).
     intro z; destruct (H z); trivial.
   Qed.
 
   Lemma bool_choice :
    (forall x:S, {R1 x} + {R2 x}) ->
-   sig
-     (fun f:S -> bool =>
-        forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x).
+     {f:S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
   Proof.
     intro H.
-    exists
-     (fun z:S => match H z with
-                 | left _ => true
-                 | right _ => false
-                 end).
+    exists (fun z:S => if H z then true else false).
     intro z; destruct (H z); auto.
   Qed.
 
 End Choice_lemmas.
 
- (** A result of type [(Exc A)] is either a normal value of type [A] or 
+Section Dependent_choice_lemmas.
+
+  Variables X : Set.
+  Variable R : X -> X -> Prop.
+
+  Lemma dependent_choice :
+    (forall x:X, {y | R x y}) ->
+    forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
+  Proof.
+    intros H x0.
+    set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
+    exists f.
+    split. reflexivity.
+    induction n; simpl; apply proj2_sig.
+  Qed.
+
+End Dependent_choice_lemmas.
+
+
+ (** A result of type [(Exc A)] is either a normal value of type [A] or
      an [error] :
 
      [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
 
-     It is implemented using the option type. *) 
+     It is implemented using the option type. *)
 
 Definition Exc := option.
 Definition value := Some.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 48b4568d..3e860fd4 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,45 +6,52 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Import Notations.
 Require Import Logic.
+Require Import Specif.
 
 (** * Useful tactics *)
 
-(** A tactic for proof by contradiction. With contradict H, 
+(** Ex falso quodlibet : a tactic for proving False instead of the current goal.
+    This is just a nicer name for tactics such as [elimtype False]
+    and other [cut False]. *)
+
+Ltac exfalso := elimtype False.
+
+(** A tactic for proof by contradiction. With contradict H,
     -   H:~A |-  B    gives       |-  A
     -   H:~A |- ~B    gives  H: B |-  A
     -   H: A |-  B    gives       |- ~A
     -   H: A |- ~B    gives  H: B |- ~A
     -   H:False leads to a resolved subgoal.
-   Moreover, negations may be in unfolded forms, 
+   Moreover, negations may be in unfolded forms,
    and A or B may live in Type *)
 
 Ltac contradict H :=
   let save tac H := let x:=fresh in intro x; tac H; rename x into H
-  in 
-  let negpos H := case H; clear H 
-  in 
+  in
+  let negpos H := case H; clear H
+  in
   let negneg H := save negpos H
   in
-  let pospos H := 
-    let A := type of H in (elimtype False; revert H; try fold (~A))
+  let pospos H :=
+    let A := type of H in (exfalso; revert H; try fold (~A))
   in
   let posneg H := save pospos H
-  in 
-  let neg H := match goal with 
+  in
+  let neg H := match goal with
    | |- (~_) => negneg H
    | |- (_->False) => negneg H
    | |- _ => negpos H
-  end in 
-  let pos H := match goal with 
+  end in
+  let pos H := match goal with
    | |- (~_) => posneg H
    | |- (_->False) => posneg H
    | |- _ => pospos H
   end in
-  match type of H with 
+  match type of H with
    | (~_) => neg H
    | (_->False) => neg H
    | _ => (elim H;fail) || pos H
@@ -52,20 +59,20 @@ Ltac contradict H :=
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
-Ltac swap H := 
+Ltac swap H :=
   idtac "swap is OBSOLETE: use contradict instead.";
   intro; apply H; clear H.
 
 (* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp H := 
+Ltac absurd_hyp H :=
   idtac "absurd_hyp is OBSOLETE: use contradict instead.";
-  let T := type of H in 
+  let T := type of H in
   absurd T.
 
 (* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
 
-Ltac false_hyp H G := 
+Ltac false_hyp H G :=
   let T := type of H in absurd T; [ apply G | assumption ].
 
 (* A case with no loss of information. *)
@@ -76,13 +83,21 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
 Tactic Notation "destruct_with_eqn" constr(x) :=
   destruct x as []_eqn.
-Tactic Notation "destruct_with_eqn" ident(n) := 
+Tactic Notation "destruct_with_eqn" ident(n) :=
   try intros until n; destruct n as []_eqn.
 Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
   destruct x as []_eqn:H.
-Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := 
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
   try intros until n; destruct n as []_eqn:H.
 
+(** Break every hypothesis of a certain type *)
+
+Ltac destruct_all t :=
+ match goal with
+  | x : t |- _ => destruct x; destruct_all t
+  | _ => idtac
+ end.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
@@ -148,7 +163,7 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
 
 (** An experimental tactic simpler than auto that is useful for ending
     proofs "in one step" *)
-  
+
 Ltac easy :=
   let rec use_hyp H :=
     match type of H with
@@ -167,14 +182,42 @@ Ltac easy :=
     solve [reflexivity | symmetry; trivial] ||
     contradiction ||
     (split; do_atom)
-  with do_ccl := trivial; repeat do_intro; do_atom in
+  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
   (use_hyps; do_ccl) || fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.
 
 (** A tactic to document or check what is proved at some point of a script *)
+
 Ltac now_show c := change c.
 
+(** Support for rewriting decidability statements *)
+
+Set Implicit Arguments.
+
+Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
+  C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
+Proof.
+intros; destruct decide. apply H0. contradiction.
+Qed.
+
+Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
+  ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
+Proof.
+intros; destruct decide. contradiction. apply H0.
+Qed.
+
+Tactic Notation "decide" constr(lemma) "with" constr(H) :=
+  let try_to_merge_hyps H :=
+     try (clear H; intro H) ||
+     (let H' := fresh H "bis" in intro H'; try clear H') ||
+     (let H' := fresh in intro H'; try clear H') in
+  match type of H with
+  | ~ ?C => apply (decide_right lemma H); try_to_merge_hyps H
+  | ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H
+  | _ => apply (decide_left lemma H); try_to_merge_hyps H
+  end.
+
 (** Clear an hypothesis and its dependencies *)
 
 Tactic Notation "clear" "dependent" hyp(h) :=
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index d3f8f1ab..3209860f 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf.v 11251 2008-07-24 08:28:40Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** * This module proves the validity of
     - well-founded recursion (also known as course of values)
@@ -65,14 +65,14 @@ Section Well_founded.
   exact (fun P:A -> Prop => well_founded_induction_type P).
  Defined.
 
-(** Well-founded fixpoints *) 
+(** Well-founded fixpoints *)
 
  Section FixPoint.
 
   Variable P : A -> Type.
   Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-  Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+  Fixpoint Fix_F (x:A) (a:Acc x) : P x :=
     F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
 
   Scheme Acc_inv_dep := Induction for Acc Sort Prop.
@@ -80,13 +80,13 @@ Section Well_founded.
   Lemma Fix_F_eq :
    forall (x:A) (r:Acc x),
      F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
-  Proof. 
+  Proof.
    destruct r using Acc_inv_dep; auto.
   Qed.
 
   Definition Fix (x:A) := Fix_F (Rwf x).
 
-  (** Proof that [well_founded_induction] satisfies the fixpoint equation. 
+  (** Proof that [well_founded_induction] satisfies the fixpoint equation.
       It requires an extra property of the functional *)
 
   Hypothesis
@@ -111,7 +111,7 @@ Section Well_founded.
 
  End FixPoint.
 
-End Well_founded. 
+End Well_founded.
 
 (** Well-founded fixpoints over pairs *)
 
@@ -120,7 +120,7 @@ Section Well_founded_2.
   Variables A B : Type.
   Variable R : A * B -> A * B -> Prop.
 
-  Variable P : A -> B -> Type. 
+  Variable P : A -> B -> Type.
 
   Section FixPoint_2.
 
@@ -129,8 +129,7 @@ Section Well_founded_2.
       forall (x:A) (x':B),
         (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
 
-  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
-   P x x' :=
+  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) : P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
          Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
new file mode 100644
index 00000000..f53d55e7
--- /dev/null
+++ b/theories/Init/vo.itarget
@@ -0,0 +1,9 @@
+Datatypes.vo
+Logic_Type.vo
+Logic.vo
+Notations.vo
+Peano.vo
+Prelude.vo
+Specif.vo
+Tactics.vo
+Wf.vo