11 files changed, 1215 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
new file mode 100755
index 000000000..19760df51
--- /dev/null
+++ b/theories/Init/Datatypes.v
@@ -0,0 +1,53 @@
+
+(* $Id$ *)
+
+(* [unit] is a singleton datatype with sole inhabitant [tt] *)
+
+Inductive unit : Set := tt : unit.
+
+(* [bool] is the datatype of the booleans values [true] and [false] *)
+
+Inductive bool : Set := true : bool 
+                      | false : bool.
+
+Add Printing If bool.
+
+(* [nat] is the datatype of natural numbers built from [O] and successor [S] *)
+(* note that zero is the letter O, not the numeral 0 *)
+
+Inductive nat : Set := O : nat 
+                     | S : nat->nat.
+
+(* [Empty_set] has no inhabitants *)
+
+Inductive Empty_set:Set :=.
+
+(* [identity A a] is a singleton datatype containing only [a] of type [A] *)
+(* the sole inhabitant is denoted [refl_identity A a] *)
+
+Inductive identity [A:Set; a:A] : A->Set :=
+     refl_identity: (identity A a a).
+Hints Resolve refl_identity : core v62.
+
+(* [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
+(* Syntax defined in Specif.v *)
+Inductive sum [A,B:Set] : Set
+    := inl : A -> (sum A B)
+     | inr : B -> (sum A B).
+
+(* [prod A B], written [A * B], is the product of [A] and [B] *)
+(* the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
+
+Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B).
+Add Printing Let prod.
+
+Section projections.
+   Variables A,B:Set.
+   Definition fst := [p:(prod A B)]Cases p of (pair x y) => x end.
+   Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end.
+End projections. 
+
+Syntactic Definition Fst := (fst ? ?).
+Syntactic Definition Snd := (snd ? ?).
+
+Hints Resolve pair inl inr : core v62.
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
new file mode 100644
index 000000000..2841c2150
--- /dev/null
+++ b/theories/Init/DatatypesSyntax.v
@@ -0,0 +1,38 @@
+
+(* $Id$ *)
+
+Require Export Datatypes.
+
+(* Parsing of things in Datatypes.v *)
+
+Grammar command command1 :=
+  pair_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "(" lcommand($c3) ","
+    lcommand($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
+| fst_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "("
+    lcommand($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
+| snd_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "("
+    lcommand($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
+
+with command0 :=
+  pair [ "(" lcommand($lc1) "," lcommand($lc2) ")" ] ->
+         [<<(pair ? ? $lc1 $lc2)>>]
+
+with command3 :=
+  prod [ command2($c1) "*" command3($c2) ] -> [<<(prod $c1 $c2)>>].
+
+(* Pretty-printing of things in Datatypes.v *)
+
+Syntax constr
+  level 4:
+    sum [<<(sum $t1 $t2)>>] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+  ;
+
+  level 3:
+    product [<<(prod $t1 $t2)>>] -> [ [<hov 0>  $t1:L [0 1] "*" $t2:E ] ]
+  ;
+
+  level 1:
+    pair
+      [<<(pair $_ $_ $t3 $t4)>>] -> [ [<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ] ]
+  | fst_imp [<<(fst $_ $_ $t2)>>] -> [ [<hov 0> "(Fst " $t2:E ")"] ]
+  | snd_imp [<<(snd $_ $_ $t2)>>] -> [ [<hov 0> "(Snd " $t2:E ")"] ].
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
new file mode 100755
index 000000000..545c0acb7
--- /dev/null
+++ b/theories/Init/Logic.v
@@ -0,0 +1,196 @@
+
+(* $Id$ *)
+
+Require Export Datatypes.
+
+(* [True] is the always true proposition *)
+Inductive True : Prop := I : True. 
+
+(* [False] is the always false proposition *)
+Inductive False : Prop := . 
+
+(* [not A], written [~A], is the negation of [A] *)
+Definition not := [A:Prop]A->False.
+
+Hints Unfold not : core.
+
+Section Conjunction.
+
+  (* [and A B], written [A /\ B], is the conjunction of [A] and [B] *)
+  (* [conj A B p q], written [<p,q>] is a proof of [A /\ B] as soon as 
+     [p] is a proof of [A] and [q] a proof of [B] *)
+  (* [proj1] and [proj2] are first and second projections of a conjunction *)
+
+  Inductive and [A,B:Prop] : Prop := conj : A -> B -> (and A B).
+
+  Variables A,B : Prop.
+
+  Theorem proj1 : (and A B) -> A.
+  Proof.
+  Induction 1; Trivial.
+  Qed.
+
+  Theorem proj2 : (and A B) -> B.
+  Proof.
+  Induction 1; Trivial.
+  Qed.
+
+End Conjunction.
+
+Section Disjunction.
+
+  (* [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
+
+  Inductive or [A,B:Prop] : Prop :=
+       or_introl : A -> (or A B) 
+     | or_intror : B -> (or A B).
+
+End Disjunction.
+
+Section Equivalence.
+
+  (* [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
+
+  Definition iff := [P,Q:Prop] (and (P->Q) (Q->P)).
+
+End Equivalence.
+
+(* [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)],
+   denotes either [P] and [Q], or [~P] and [Q] *)
+Definition IF := [P,Q,R:Prop] (or (and P Q) (and (not P) R)).
+
+Section First_order_quantifiers.
+
+  (* [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an 
+     [x] of type [A] which satisfies the predicate [P] ([A] is of type 
+     [Set]). This is existential quantification. *)
+
+  (* [(ex2 A P Q)], or simply [(EX x | P(x) & Q(x))], expresses the
+     existence of an [x] of type [A] which satisfies both the predicates
+     [P] and [Q] *)
+
+  (* Universal quantification (especially first-order one) is normally 
+     written [(x:A)(P x)]. For duality with existential quantification, the 
+     construction [(all A P)], or simply [(All P)], is provided as an 
+     abbreviation of [(x:A)(P x)] *) 
+
+  Inductive ex [A:Set;P:A->Prop] : Prop 
+      := ex_intro : (x:A)(P x)->(ex A P).
+
+  Inductive ex2 [A:Set;P,Q:A->Prop] : Prop
+      := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
+
+  Definition all := [A:Set][P:A->Prop](x:A)(P x). 
+
+End First_order_quantifiers.
+
+Section Equality.
+
+  (* [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality
+     of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+     The definition is inductive and states the reflexivity of the equality.
+     The others properties (symmetry, transitivity, replacement of 
+     equals) are proved below *)
+
+  Inductive eq [A:Set;x:A] : A->Prop
+         := refl_equal : (eq A x x).
+
+End Equality.
+
+Hints Resolve I conj or_introl or_intror refl_equal : core v62.
+Hints Resolve ex_intro ex_intro2 : core v62.
+
+Section Logic_lemmas.
+
+  Theorem absurd : (A:Prop)(C:Prop) A -> (not A) -> C.
+  Proof.
+    Unfold not; Intros A C h1 h2.
+    Elim (h2 h1).
+  Qed.
+
+  Section equality.
+    Variable A,B : Set.
+    Variable f   : A->B.
+    Variable x,y,z : A.
+
+    Theorem sym_eq : (eq ? x y) -> (eq ? y x).
+    Proof.
+     Induction 1; Trivial.
+    Qed.
+
+    Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z).
+    Proof.
+     Induction 2; Trivial.
+    Qed.
+
+    Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)).
+    Proof.
+     Induction 1; Trivial.
+    Qed.
+
+    Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)).
+    Proof.
+     Red; Intros h1 h2; Apply h1; Elim h2; Trivial.
+    Qed.
+
+    Definition sym_equal     := sym_eq.
+    Definition sym_not_equal := sym_not_eq.
+    Definition trans_equal   := trans_eq.
+
+  End equality.
+
+  Theorem eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
+  Proof.
+   Intros.
+   Cut (identity A x y).
+   Destruct 1; Auto.
+   Elim H; Auto.
+  Qed.
+
+  Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y).
+   Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  Defined.
+
+  Definition eq_rec_r : (A:Set)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y).
+    Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  Defined.
+
+  Definition eq_rect_r : (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y).
+    Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
+  Defined.
+End Logic_lemmas.
+
+Theorem f_equal2 : (A1,A2,B:Set)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2)
+  (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? (f x1 x2) (f y1 y2)).
+Proof.
+  Induction 1; Induction 1; Trivial.
+Qed.
+
+Theorem f_equal3 : (A1,A2,A3,B:Set)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2)
+  (x3,y3:A3)(eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) 
+   -> (eq ? (f x1 x2 x3) (f y1 y2 y3)).
+Proof.
+  Induction 1; Induction 1; Induction 1; Trivial.
+Qed.
+
+Theorem f_equal4 : (A1,A2,A3,A4,B:Set)(f:A1->A2->A3->A4->B)
+  (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)
+  (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4)
+   -> (eq ? (f x1 x2 x3 x4) (f y1 y2 y3 y4)).
+Proof.
+  Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
+Qed.
+
+Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Set)(f:A1->A2->A3->A4->A5->B)
+  (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)(x5,y5:A5)
+  (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4) -> (eq ? x5 y5)
+    -> (eq ? (f x1 x2 x3 x4 x5) (f y1 y2 y3 y4 y5)).
+Proof.
+  Induction 1; Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
+Qed.
+
+Hints Immediate sym_eq sym_not_eq : core v62.
+
+Syntactic Definition Ex := ex | 1.
+Syntactic Definition Ex2 := ex2 | 1.
+Syntactic Definition All := all | 1.
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
new file mode 100644
index 000000000..aac5a7532
--- /dev/null
+++ b/theories/Init/LogicSyntax.v
@@ -0,0 +1,92 @@
+
+(* $Id$ *)
+
+Require Export Logic.
+
+(* Parsing of things in Logic.v *)
+
+Grammar command command1 :=
+  conj [ "<" lcommand($l1) "," lcommand($c2) ">" "{" command($c3) ","
+        command($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
+| proj1 [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "{"
+        lcommand($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
+| proj2 [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "{"
+        lcommand($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
+| IF [ "either" command($c) "and_then" command($t) "or_else" command($e) ] ->
+       [<<(IF $c $t $e)>>]
+| all [ "<" lcommand($l1) ">" "All" "(" lcommand($l2) ")" ] ->
+       [<<(all $l1 $l2)>>]
+| eq_expl [ "<" lcommand($l1) ">" command0($c1) "=" command0($c2) ] ->
+            [<<(eq $l1 $c1 $c2)>>]
+| eq_impl [ command0($c) "=" command0($c2) ] -> [<<(eq ? $c $c2)>>]
+
+with command2 :=
+  not [ "~" command2($c) ] -> [<<(not $c)>>]
+
+with command6 :=
+  and [ command5($c1) "/\\" command6($c2) ] -> [<<(and $c1 $c2)>>]
+
+with command7 :=
+  or [ command6($c1) "\\/" command7($c2) ] -> [<<(or $c1 $c2)>>]
+
+with command8 :=
+  iff [ command7($c1) "<->" command8($c2) ] -> [<<(iff $c1 $c2)>>]
+
+with command10 :=
+  allexplicit [ "ALL" ident($x) ":" command($t) "|" command($p) ]
+                          -> [<<(all $t [$x:$t]$p)>>]
+| allimplicit [ "ALL" ident($x) "|" command($p) ]
+                          -> [<<(all ? [$x]$p)>>]
+| exexplicit [ "EX" ident($v) ":" command($t) "|" command($c1) ]
+                          -> [<<(ex $t [$v:$t]$c1)>>]
+| eximplicit [ "EX" ident($v) "|" command($c1) ] 
+                          -> [<<(ex ? [$v]$c1)>>]
+| ex2explicit [ "EX" ident($v) ":" command($t) "|" command($c1) "&"
+           command($c2) ] -> [<<(ex2 $t [$v:$t]$c1 [$v:$t]$c2)>>]
+| ex2implicit [ "EX" ident($v) "|" command($c1) "&" 
+           command($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
+
+
+(* Pretty-printing of things in Logic.v *)
+
+Syntax constr
+  level 1:
+    equal [<<(eq $_  $t1  $t2)>>] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+  | conj [<<(conj $t1 $t2 $t3 $t4)>>]
+      -> [ [<hov 1> [<hov 1> "<" $t1:L "," [0 0] $t2:L ">" ] [0 0]
+                    [<hov 1> "{" $t3:L "," [0 0] $t4:L "}"] ] ]
+  | IF [<< either $c and_then $t or_else $e >>]
+      -> [ [<hov 0> "either" [1 1] $c:E
+                [<hov 0> [1 1] "and_then" [1 1] $t:E ]
+                [<hov 0> [1 1] "or_else" [1 1] $e:E ]] ]
+  ;
+
+  level 2:
+    not [<< ~ $t1 >>] -> [ [<hov 0> "~" $t1:E ] ]
+  ;
+
+  level 6:
+    and [<< $t1 /\ $t2 >>] -> [ [<hov 0> $t1:L [0 0] "/\\" $t2:E ] ]
+  ;
+
+  level 7:
+    or [<< $t1 \/ $t2 >>] -> [ [<hov 0> $t1:L [0 0]  "\\/" $t2:E ] ]
+  ;
+
+  level 8:
+    iff [<< $t1 <-> $t2 >>] -> [ [<hov 0> $t1:L [0 0] "<->" $t2:E ] ]
+  ;
+
+  level 10:
+    all_pred [<<(all $_ $p)>>] -> [ [<hov 4> "All " $p:L ] ]
+  | all_imp [<<(all $_ [$x:$T]$t)>>]
+       -> [ [<hov 3> "ALL " $x ":" $T:L " |" [1 0] $t:L ] ]
+
+  | ex_pred [<<(ex $_ $p)>>] -> [ [<hov 0> "Ex " $p:L ] ]
+  | ex [<<(ex $_ [$x:$T]$P)>>] 
+       -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 0] $P:L ] ]
+
+  | ex2_pred [<<(ex2 $_ $p1 $p2)>>]
+       -> [ [<hov 3> "Ex2 " $p1:L [1 0] $p2:L ] ]
+  | ex2 [<<(ex2 $_ [$x:$T]$P1 [$x:$T]$P2)>>] 
+       -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ].
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
new file mode 100755
index 000000000..1cd3ad8be
--- /dev/null
+++ b/theories/Init/Logic_Type.v
@@ -0,0 +1,173 @@
+
+(* $Id$ *)
+
+(* This module defines quantification on the world [Type] *)
+(* [Logic.v] was defining it on the world [Set] *)
+
+Require Export Logic.
+Require LogicSyntax.
+
+
+(* [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
+   when [A] is of type [Type] *)
+
+Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
+
+Section universal_quantification.
+
+Variable A : Type.
+Variable P : A->Prop.
+
+Theorem inst :  (x:A)(allT ? [x](P x))->(P x).
+Proof.
+Unfold allT; Auto.
+Qed.
+
+Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT A P).
+Proof.
+Red; Auto.
+Qed.
+
+End universal_quantification.
+
+(* Existential Quantification *)
+
+(* [exT A P], or simply [(EXT x | P(x))], stands for the existential 
+   quantification on the predicate [P] when [A] is of type [Type] *)
+
+(* [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the
+   existential quantification on both [P] and [Q] when [A] is of
+   type [Type] *)
+
+Inductive  exT [A:Type;P:A->Prop] : Prop
+    := exT_intro : (x:A)(P x)->(exT A P).
+
+Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
+    := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
+
+(* Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) *)
+(* [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of 
+   type [Type]. This equality satisfies reflexivity (by definition), 
+   symmetry, transitivity and stability by congruence *)
+
+Inductive eqT [A:Type;x:A] : A -> Prop
+                       := refl_eqT : (eqT A x x).
+
+Hints Resolve refl_eqT exT_intro2 exT_intro : core v62.
+
+Section Equality_is_a_congruence.
+
+ Variables A,B : Type.
+ Variable  f : A->B.
+
+ Variable x,y,z : A.
+ 
+ Lemma sym_eqT : (eqT ? x y) -> (eqT ? y x).
+ Proof.
+  Induction 1; Trivial.
+ Qed.
+
+ Lemma trans_eqT : (eqT ? x y) -> (eqT ? y z) -> (eqT ? x z).
+ Proof.
+  Induction 2; Trivial.
+ Qed.
+
+ Lemma congr_eqT : (eqT ? x y)->(eqT ? (f x) (f y)).
+ Proof.
+  Induction 1; Trivial.
+ Qed.
+
+ Lemma sym_not_eqT : ~(eqT ? x y) -> ~(eqT ? y x).
+ Proof.
+  Red; Intros H H'; Apply H; Elim H'; Trivial.
+ Qed.
+
+End Equality_is_a_congruence.
+
+Hints Immediate sym_eqT sym_not_eqT : core v62.
+
+(* This states the replacement of equals by equals in a proposition *)
+
+Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
+Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
+Defined.
+
+(*** not allowed because of dependencies 
+Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y).
+Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
+Defined.
+****)
+
+(* Some datatypes at the [Type] level *)
+
+Inductive EmptyT: Type :=.
+Inductive UnitT : Type := IT : UnitT.
+
+Definition notT := [A:Type] A->EmptyT.
+
+(* Have you an idea of what means [identityT A a b] ? No matter ! *)
+
+Inductive identityT [A:Type; a:A] : A->Type :=
+     refl_identityT : (identityT A a a).
+
+Hints Resolve refl_identityT : core v62.
+
+Section IdentityT_is_a_congruence.
+
+ Variables A,B : Type.
+ Variable  f : A->B.
+
+ Variable x,y,z : A.
+ 
+ Lemma sym_idT : (identityT ? x y) -> (identityT ? y x).
+ Proof.
+  Induction 1; Trivial.
+ Qed.
+
+ Lemma trans_idT : (identityT ? x y) -> (identityT ? y z) -> (identityT ? x z).
+ Proof.
+  Induction 2; Trivial.
+ Qed.
+
+ Lemma congr_idT : (identityT ? x y)->(identityT ? (f x) (f y)).
+ Proof.
+  Induction 1; Trivial.
+ Qed.
+
+ Lemma sym_not_idT : (notT (identityT ? x y)) -> (notT (identityT ? y x)).
+ Proof.
+  Red; Intros H H'; Apply H; Elim H'; Trivial.
+ Qed.
+
+End IdentityT_is_a_congruence.
+
+Definition identityT_ind_r :
+     (A:Type)
+        (a:A)
+         (P:A->Prop)
+          (P a)->(y:A)(identityT ? y a)->(P y).
+ Intros A x P H y H0; Case sym_idT with 1:= H0; Trivial.
+Defined.
+
+Definition identityT_rec_r :      
+     (A:Type)
+        (a:A)
+         (P:A->Set)
+          (P a)->(y:A)(identityT ? y a)->(P y).
+ Intros A x P H y H0; Case sym_idT with 1:= H0; Trivial.
+Defined.
+
+Definition identityT_rect_r :      
+     (A:Type)
+        (a:A)
+         (P:A->Type)
+          (P a)->(y:A)(identityT ? y a)->(P y).
+ Intros A x P H y H0; Case sym_idT with 1:= H0; Trivial.
+Defined.
+
+Hints Immediate sym_idT sym_not_idT : core v62.
+
+
+Syntactic Definition AllT := allT | 1.
+Syntactic Definition ExT := exT | 1.
+Syntactic Definition ExT2 := exT2 | 1.
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
new file mode 100644
index 000000000..7ae7ffa90
--- /dev/null
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -0,0 +1,52 @@
+
+(* $Id$ *)
+
+Require Logic_Type.
+
+(* Parsing of things in Logic_type.v *)
+
+Grammar command command1 :=
+  eqT_expl [ "<" lcommand($l1) ">" command0($c1) "==" command0($c2) ] ->
+          [<<(eqT $l1 $c1 $c2)>>]
+| eqT_impl [ command0($c) "==" command0($c2) ] -> [<<(eqT ? $c $c2)>>]
+| idT_expl [ "<" lcommand($l1) ">" command0($c1) "===" command0($c2) ] ->
+          [<<(identityT $l1 $c1 $c2)>>]
+| idT_impl [ command0($c) "===" command0($c2) ] -> [<<(identityT ? $c $c2)>>]
+
+with command10 :=
+  allTexplicit [ "ALLT" ident($v) ":" command($t) "|" command($c1) ]
+                          -> [<<(allT $t [$v:$t]$c1)>>]
+| allTimplicit [ "ALLT" ident($v) "|" command($c1) ] 
+                          -> [<<(allT ? [$v]$c1)>>]
+| exTexplicit [ "EXT" ident($v) ":" command($t) "|" command($c1) ]
+                          -> [<<(exT $t [$v:$t]$c1)>>]
+| exTimplicit [ "EXT" ident($v) "|" command($c1) ] 
+                          -> [<<(exT ? [$v]$c1)>>]
+| exT2explicit [ "EXT" ident($v) ":" command($t) "|" command($c1) "&"
+           command($c2) ] -> [<<(exT2 $t [$v:$t]$c1 [$v:$t]$c2)>>]
+| exT2implicit [ "EXT" ident($v) "|" command($c1) "&" 
+           command($c2) ] -> [<<(exT2 ? [$v]$c1 [$v]$c2)>>].
+
+(* Pretty-printing of things in Logic_type.v *)
+
+Syntax constr
+  level 10:
+    allT_pred [<<(allT $_ $p)>>] -> [ [<hov 0> "AllT " $p:L ] ]
+  | allT [<<(allT $T [$x:$T]$p)>>]
+       -> [ [<hov 3> "ALLT " $x ":" $T:L " |" [1 0] $p:L ] ]
+
+  | exT_pred [<<(exT $_ $p)>>] -> [ [<hov 4> "ExT " $p:L ] ]
+  | exT [<<(exT $t1 [$x:$T]$p)>>] 
+       -> [ [<hov 4> "EXT " $x ":" $T:L " |" [1 0] $p:L ] ]
+
+  | exT2_pred [<<(exT2 $_ $p1 $p2)>>]
+       -> [ [<hov 4> "ExT2 " $p1:L [1 0] $p2:L ] ]
+  | exT2 [<<(exT2 $T [$x:$T]$P1 [$x:$T]$P2)>>] 
+       -> [ [<hov 2> "EXT " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ]
+  ;
+
+  level 1:
+    eqT [<<(eqT $_ $c1 $c2)>>] -> [ [<hov 1> $c1:E [0 0] "==" $c2:E ] ]
+
+  | identityT [<<(identityT $_ $c1 $c2)>>]
+       -> [ [<hov 1> $c1:E [0 0] "===" $c2:E ] ].
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
new file mode 100755
index 000000000..b8bf598af
--- /dev/null
+++ b/theories/Init/Peano.v
@@ -0,0 +1,158 @@
+
+(* $Id$ *)
+
+(* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
+(* This module defines the following operations on natural numbers :
+     - predecessor [pred]
+     - addition [plus]
+     - multiplication [mult]
+     - less or equal order [le]
+     - less [lt]
+     - greater or equal [ge]
+     - greater [gt]
+   This module states various lemmas and theorems about natural numbers,
+   including Peano's axioms of arithmetic (in Coq, these are in fact provable)
+   Case analysis on [nat] and induction on [nat * nat] are provided too *)
+
+Require Export Logic.
+Require Export LogicSyntax.
+Require Export Datatypes.
+
+Definition eq_S := (f_equal nat nat S).
+
+Hint eq_S : v62 := Resolve (f_equal nat nat S).
+Hint eq_nat_unary : core := Resolve (f_equal nat).
+
+(* The predecessor function *)
+
+Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end).
+Hint eq_pred : v62 := Resolve (f_equal nat nat pred).
+
+Theorem pred_Sn : (m:nat) m=(pred (S m)).
+ Proof.
+Auto.
+Qed.
+
+Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
+Proof.
+  Intros n m H ; Change (pred (S n))=(pred (S m)); Auto.
+Qed.
+
+Hints Immediate eq_add_S : core v62.
+
+(* A consequence of the previous axioms *)
+
+Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
+Proof.
+ Red; Auto.
+Qed.
+Hints Resolve not_eq_S : core v62.
+
+Definition IsSucc : nat->Prop
+  := [n:nat]Cases n of O => False | (S p) => True end.
+
+
+Theorem O_S : (n:nat)~(O=(S n)).
+Proof.
+  Red;Intros n H.
+  Change (IsSucc O).
+  Elim (sym_eq nat O (S n));[Exact I | Assumption].
+Qed.
+Hints Resolve O_S : core v62.
+
+Theorem n_Sn : (n:nat) ~(n=(S n)).
+Proof.
+ Induction n ; Auto.
+Qed.
+Hints Resolve n_Sn : core v62.
+
+(*************************************************)
+(*      Addition                                 *)
+(*************************************************)
+
+Fixpoint plus [n:nat] : nat -> nat := 
+   [m:nat]Cases n of 
+      O   => m 
+  | (S p) => (S (plus p m)) end.
+Hint eq_plus : v62 := Resolve (f_equal2 nat nat nat plus).
+Hint eq_nat_binary : core := Resolve (f_equal2 nat nat).
+
+Lemma plus_n_O : (n:nat) n=(plus n O).
+Proof.
+ Induction n ; Simpl ; Auto.
+Qed.
+Hints Resolve plus_n_O : core v62.
+
+Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
+Proof.
+ Intros m n; Elim m; Simpl; Auto.
+Qed.
+Hints Resolve plus_n_Sm : core v62.
+
+(***************************************)
+(*      Multiplication                 *)
+(***************************************)
+
+Fixpoint  mult [n:nat] : nat -> nat := 
+   [m:nat]Cases n of O => O 
+               | (S p) => (plus m (mult p m)) end.
+Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
+
+Lemma mult_n_O : (n:nat) O=(mult n O).
+Proof.
+ Induction n; Simpl; Auto.
+Qed.
+Hints Resolve mult_n_O : core v62.
+
+Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
+Proof.
+ Intros; Elim n; Simpl; Auto.
+ Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S).
+ Pattern 1 3 m; Elim m; Simpl; Auto.
+Qed.
+Hints Resolve mult_n_Sm : core v62.
+
+(***********************************************************************)
+(* Definition of the usual orders, the basic properties of le and lt   *)
+(* can be found in files Le and Lt                                     *)
+(***********************************************************************)
+
+(* An inductive definition to define the order *)
+
+Inductive le [n:nat] : nat -> Prop
+    := le_n : (le n n)
+     | le_S : (m:nat)(le n m)->(le n (S m)).
+
+Hint constr_le : core v62 := Constructors le.
+(* equivalent to : "Hints Resolve le_n le_S : core v62." *)
+
+Definition lt := [n,m:nat](le (S n) m).
+Hints Unfold lt : core v62.
+
+Definition ge := [n,m:nat](le m n).
+Hints Unfold ge : core v62.
+
+Definition gt := [n,m:nat](lt m n).
+Hints Unfold gt : core v62.
+
+(*********************************************************)
+(* Pattern-Matching on natural numbers                   *)
+(*********************************************************)
+
+Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
+Proof.
+ Induction n ; Auto.
+Qed.
+
+(**********************************************************)
+(* Principle of double induction                          *)
+(**********************************************************)
+
+Theorem nat_double_ind : (R:nat->nat->Prop)
+     ((n:nat)(R O n)) -> ((n:nat)(R (S n) O))
+     -> ((n,m:nat)(R n m)->(R (S n) (S m)))
+     -> (n,m:nat)(R n m).
+Proof.
+ Induction n; Auto.
+ Induction m; Auto.
+Qed.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
new file mode 100755
index 000000000..c80278aaa
--- /dev/null
+++ b/theories/Init/Prelude.v
@@ -0,0 +1,11 @@
+
+(* $Id$ *)
+
+Require Export Datatypes.
+Require Export DatatypesSyntax.
+Require Export Logic.
+Require Export LogicSyntax.
+Require Export Specif.
+Require Export SpecifSyntax.
+Require Export Peano.
+Require Export Wf.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
new file mode 100755
index 000000000..53d3dd136
--- /dev/null
+++ b/theories/Init/Specif.v
@@ -0,0 +1,214 @@
+
+(* $Id$ *)
+
+(**************************************************************)
+(* Basic specifications : Sets containing logical information *)
+(**************************************************************)
+
+Require Export Logic.
+Require LogicSyntax.
+
+Section Subsets.
+
+  (* [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset 
+     of elements of the Set [A] which satisfy the predicate [P].
+     Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset 
+     of elements of the Set [A] which satisfy both [P] and [Q]. *)
+
+  Inductive sig [A:Set;P:A->Prop] : Set
+      := exist : (x:A)(P x) -> (sig A P).
+
+  Inductive sig2 [A:Set;P,Q:A->Prop] : Set
+      := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q).
+
+  (* [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
+     of subset where [P] is now of type [Set].
+     Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
+     
+  Inductive sigS [A:Set;P:A->Set] : Set
+      := existS : (x:A)(P x) -> (sigS A P).
+
+  Inductive sigS2 [A:Set;P,Q:A->Set] : Set
+      := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q).
+
+End Subsets.
+
+Add Printing Let sig.
+Add Printing Let sig2.
+Add Printing Let sigS.
+Add Printing Let sigS2.
+
+
+(***********************)
+(* Projections of sig *)
+(***********************)
+
+Section Subset_projections.
+
+  Variable A:Set.
+  Variable P:A->Prop.
+
+  Definition proj1_sig :=
+   [e:(sig A P)]Cases e of (exist a b) => a  end.
+
+  Definition proj2_sig :=
+   [e:(sig A P)]
+     <[e:(sig A P)](P (proj1_sig e))>Cases e of (exist a b) => b  end.
+
+End Subset_projections.
+
+
+(***********************)
+(* Projections of sigS *)
+(***********************)
+
+Section Projections.
+
+  Variable A:Set.
+  Variable P:A->Set.
+
+  (* An element [y] of a subset [[{x:A & (P x)}] is the pair of an [a] of 
+     type [A] and of a proof [h] that [a] satisfies [P].
+     Then [(projS1 y)] is the witness [a]
+     and [(projS2 y)] is the proof of [(P a)] *)
+
+  Definition projS1 (* : (A:Set)(P:A->Set)(sigS A P) -> A *)
+           := [x:(sigS A P)]Cases x of (existS a _) => a end.
+  Definition projS2 (* : (A:Set)(P:A->Set)(H:(sigS A P))(P (projS1 A P H)) *)
+           := [x:(sigS A P)]<[x:(sigS A P)](P (projS1 x))> 
+                  Cases x of (existS _ h) => h end.
+
+End Projections.
+
+Syntactic Definition ProjS1 := (projS1 ? ?).
+Syntactic Definition ProjS2 := (projS2 ? ?).
+
+
+Section Extended_booleans.
+
+  (* Syntax sumbool "{_}+{_}". *)
+  Inductive sumbool [A,B:Prop] : Set
+      := left  : A -> (sumbool A B) 
+       | right : B -> (sumbool A B).
+
+  (* Syntax sumor "_+{_}". *)
+  Inductive sumor [A:Set;B:Prop] : Set
+      := inleft  : A -> (sumor A B) 
+       | inright : B -> (sumor A B).
+
+
+End Extended_booleans.
+
+
+(**********)
+(* Choice *)
+(**********)
+
+Section Choice_lemmas.
+
+  (* The following lemmas state various forms of the axiom of choice *)
+
+  Variables S,S':Set.
+  Variable R:S->S'->Prop.
+  Variable R':S->S'->Set.
+  Variables R1,R2 :S->Prop.
+
+  Lemma Choice : ((x:S)(sig ? [y:S'](R x y))) ->
+                     (sig ? [f:S->S'](z:S)(R z (f z))).
+  Proof.
+   Intro H.
+   Exists [z:S]Cases (H z) of (exist y _) => y end.
+   Intro z; Elim (H z); Trivial.
+  Qed.
+
+  Lemma Choice2 : ((x:S)(sigS ? [y:S'](R' x y))) ->
+                     (sigS ? [f:S->S'](z:S)(R' z (f z))).
+  Proof.
+    Intro H.
+    Exists [z:S]Cases (H z) of (existS y _) => y end.
+    Intro z; Elim (H z); Trivial.
+  Qed.
+
+  Lemma bool_choice : 
+    ((x:S)(sumbool (R1 x) (R2 x))) ->
+    (sig ? [f:S->bool] (x:S)( ((f x)=true  /\ (R1 x)) 
+                           \/ ((f x)=false /\ (R2 x)))).
+  Proof.
+    Intro H.
+    Exists [z:S]Cases (H z) of (left _) => true | (right _) => false end.
+    Intro z; Elim (H z); Auto.
+  Qed.
+
+End Choice_lemmas.
+
+Section Exceptions.
+
+  (* A result of type [(Exc A)] is either a normal value of type [A] or 
+     an [error]. *) 
+
+  Inductive Exc [A:Set] : Set := value : A->(Exc A) 
+                               | error : (Exc A).
+
+End Exceptions.
+
+Syntactic Definition Error := (error ?).
+Syntactic Definition Value := (value ?).
+
+
+(*******************************)
+(* Self realizing propositions *)
+(*******************************)
+
+Axiom False_rec : (P:Set)False->P.
+
+Lemma False_rect: (C:Type)False->C.
+Proof.
+  Intros.
+  Cut Empty_set.
+  Destruct 1.
+  Elim H.
+Qed.
+
+
+Definition except := False_rec. (* for compatibility with previous versions *)
+
+Syntactic Definition Except := (except ?).
+
+Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
+Proof.
+  Intros A C h1 h2.
+  Apply False_rec.
+  Apply (h2 h1).
+Qed.
+
+Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C.
+Proof.
+  Intros A B C F AB; Apply F; Elim AB; Auto.
+Qed.
+
+(** is now a theorem
+Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b).
+**)
+
+Hints Resolve left right inleft inright : core v62.
+
+(*********************************)
+(* Sigma Type at Type level sigT *)
+(*********************************)
+
+Inductive sigT [A:Type;P:A->Type] : Type
+    := existT : (x:A)(P x) -> (sigT A P).
+
+Section projections_sigT.
+
+  Variable A:Type.
+  Variable P:A->Type.
+
+  Definition projT1 (* : (A:Type)(P:A->Type)(sigT A P) -> A *)
+              := [H:(sigT A P)]Cases H of (existT x _) => x end.
+   
+  Definition projT2 (* : (A:Type)(P:A->Type)(p:(sigT A P))(P (projT1 A P p)) *)
+              := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))> 
+                     Cases H of (existT x h) => h end.
+
+End projections_sigT.
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
new file mode 100644
index 000000000..1b78cd522
--- /dev/null
+++ b/theories/Init/SpecifSyntax.v
@@ -0,0 +1,125 @@
+
+(* $Id$ *)
+
+Require Export LogicSyntax.
+Require Export Specif.
+
+(* Parsing of things in Specif.v *)
+
+Grammar command command1 :=
+  sig [ "{" lcommand($lc) ":" lcommand($c1) "|" lcommand($c2) "}" ]
+       -> [<<(sig $c1 [$lc:$c1]$c2)>>]
+
+| sig2 [ "{" lcommand($lc) ":" lcommand($c1)
+           "|" lcommand($c2) "&" lcommand($c3) "}" ]
+       -> [<<(sig2 $c1 [$lc:$c1]$c2 [$lc:$c1]$c3)>>]
+
+| sigS [ "{" lcommand($lc) ":" lcommand($c1) "&" lcommand($c2) "}" ]
+       -> [<<(sigS $c1 [$lc:$c1]$c2)>>]
+
+| sigS2 [ "{" lcommand($lc) ":" lcommand($c1)
+             "&" lcommand($c2) "&" lcommand($c3) "}" ]
+       -> [<<(sigS2 $c1 [$lc:$c1]$c2 [$lc:$c1]$c3)>>]
+
+| squash [ "{" lcommand($lc) "}" ] -> [(SQUASH $lc)].
+
+Grammar command lassoc_command4 :=
+  squash_sum
+  [ lassoc_command4($c1) "+" lassoc_command4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [<<(sumbool $T1 $T2)>>] (* {T1}+{T2} *)
+            | $_           -> [<<(sumor $c1 $T2)>>]   (* c1+{T2} *)
+            esac
+      | $_           -> [<<(sum $c1 $c2)>>]           (* c1+c2 *)
+      esac.
+
+(* Pretty-printing of things in Specif.v *)
+
+Syntax constr
+  (* Default pretty-printing rules *)
+  level 10:
+    sig_var
+      [(ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ]
+  | sig2_var
+      [(Sig2_ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L ] ]
+  | sigS_var
+      [(SigS_ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sigS " $c1:L [1 1] $c2:L ] ]
+  | sigS2_var [(SigS2_ABSTR_B_NB $c1 $c2 $c3)]
+      -> [ [<hov 0> "sigS2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ]
+  ;
+
+  level 1:
+(* Pretty-printing of [sig] *)
+    sig  [<<(sig $c1 $c2)>>] -> [ (ABSTR_B_NB  $c1 $c2):E ]
+  | sig_nb [(ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2))]
+      -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ]
+  | sigma_b [(ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2))]
+      -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ]
+
+(* Pretty-printing of [sig2] *)
+  | sig2 [<<(sig2 $c1 $c2 $c3)>>] -> [ (Sig2_ABSTR_B_NB  $c1 $c2 $c3):E ]
+  | sig2_b_b
+      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                            (LAMBDALIST $c1 [$id]$c3))]
+       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sig2_nb_b
+      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                            (LAMBDALIST  $c1 [$id]$c3))]
+       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sig2_b_nb
+      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                            (LAMBDALIST $c1 [<>]$c3))]
+       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sig2_nb_nb
+      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                            (LAMBDALIST $c1 [<>]$c3))]
+       -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ]
+
+(* Pretty-printing of [sigS] *)
+  | sigS [<<(sigS $c1 $c2)>>] -> [(SigS_ABSTR_B_NB  $c1 $c2):E]
+  | sigS_nb [(SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2))]
+       -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E  "}" ] ]
+  | sigS_b [(SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2))]
+       -> [ [<hov 0> "{" $id  ":" $c1:E [1 3] "& " $c2:E "}" ] ]
+
+(* Pretty-printing of [sigS2] *)
+  | sigS2 [<<(sigS2 $c1 $c2 $c3)>>] -> [(SigS2_ABSTR_B_NB  $c1 $c2 $c3):E]
+  | sigS2_b_b
+      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                             (LAMBDALIST $c1 [$id]$c3))]
+       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sigS2_nb_b
+      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                             (LAMBDALIST  $c1 [$id]$c3))]
+       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sigS2_b_nb
+      [ (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                              (LAMBDALIST $c1 [<>]$c3))]
+       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
+  | sigS2_nb_nb
+      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                             (LAMBDALIST $c1 [<>]$c3))]
+       -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
+
+(* Pretty-printing of [projS1] and [projS2] *)
+  | projS1_imp [<<(projS1 ? ? $a)>>] -> ["(ProjS1 " $a:E ")"]  
+  | projS2_imp [<<(projS2 ? ? $a)>>] -> ["(ProjS2 " $a:E ")"]
+  ;
+
+(* Pretty-printing of [sumbool] and [sumor] *)
+  level 4:
+    sumbool [<<(sumbool $t1 $t2)>>]
+       -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ]
+  | sumor [<<(sumor $t1 $t2)>>]
+       -> [ [<hov 0> $t1:E [0 1]  "+" "{" $t2:L "}"] ]
+  ;
+
+(* Pretty-printing of [except] *)
+  level 1:
+    Except_imp [<<(except $1 $t2)>>] -> [ [<hov 0> "Except " $t2 ] ]
+
+(* Pretty-printing of [error] and [value] *)
+  | Error_imp [<<(error $1 $t2)>>] -> [ [<hov 0> "Error " $t2 ] ]
+  | Value_imp [<<(value $1 $t2)>>] -> [ [<hov 0> "Value " $t2 ] ].
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
new file mode 100755
index 000000000..454ca5dff
--- /dev/null
+++ b/theories/Init/Wf.v
@@ -0,0 +1,103 @@
+
+(* $Id$ *)
+
+(* This module proves the validity of
+    - well-founded recursion (also called course of values)
+    - well-founded induction
+   from a well-founded ordering on a given set *)
+
+Require Export Logic.
+Require Export LogicSyntax.
+
+(* Well-founded induction principle on Prop *)
+
+Chapter Well_founded.
+
+ Variable A : Set.
+ Variable R : A -> A -> Prop.
+
+ (* The accessibility predicate is defined to be non-informative *)
+
+ Inductive  Acc : A -> Prop 
+    := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
+
+ Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
+  Destruct 1; Trivial.
+ Defined.
+
+  (* the informative elimination :
+     let Acc_rec F = let rec wf x = F x wf in wf *)
+
+ Section AccRec.
+  Variable P : A -> Set.
+  Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x).
+
+  Fixpoint Acc_rec [x:A;a:(Acc x)] : (P x)
+     := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rec y (Acc_inv x a y h)))).
+
+ End AccRec.
+
+ (* A relation is well-founded if every element is accessible *)
+
+ Definition well_founded := (a:A)(Acc a).
+
+ (* well-founded induction on Set and Prop *)
+
+ Hypothesis Rwf : well_founded.
+
+ Theorem well_founded_induction : 
+        (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+ Proof.
+  Intros; Apply (Acc_rec P); Auto.
+ Save.
+
+  Theorem well_founded_ind : 
+         (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+   Proof.
+    Intros; Apply (Acc_ind P); Auto.
+   Qed.
+
+(* Building fixpoints  *) 
+
+Section FixPoint.
+
+Variable P : A -> Set.
+Variable F : (x:A)((y:A)(R y x)->(P y))->(P x).
+
+Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := 
+         (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))).
+
+Definition fix := [x:A](Fix_F x (Rwf x)).
+
+(* Proof that well_founded_induction satisfies the fixpoint equation. 
+   It requires an extra property of the functional *)
+
+Hypothesis F_ext : 
+  (x:A)(f,g:(y:A)(R y x)->(P y))
+  ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g).
+
+Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+
+Lemma Fix_F_eq
+  : (x:A)(r:(Acc x))
+    (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r).
+Intros x r; Elim r using  Acc_inv_dep; Auto.
+Save.
+
+Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s).
+Intro x; Elim (Rwf x); Intros.
+Case (Fix_F_eq x0 r); Case (Fix_F_eq x0 s); Intros.
+Apply F_ext; Auto.
+Save.
+
+
+Lemma fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)).
+Intro; Unfold fix.
+Case (Fix_F_eq x).
+Apply F_ext; Intros.
+Apply Fix_F_inv.
+Save.
+
+End FixPoint.
+
+End Well_founded.