Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

8 files changed, 413 insertions, 421 deletions

diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v
index 55259b943..4223a0547 100644
--- a/contrib/correctness/ArrayPermut.v
+++ b/contrib/correctness/ArrayPermut.v
@@ -15,11 +15,11 @@
 (*                        Definition and properties                         *)
 (****************************************************************************)
 
-Require ProgInt.
-Require Arrays.
+Require Import ProgInt.
+Require Import Arrays.
 Require Export Exchange.
 
-Require Omega.
+Require Import Omega.
 
 Set Implicit Arguments.
 
@@ -27,18 +27,16 @@ Set Implicit Arguments.
  * transpositions i.e. exchange of two elements.
  *)
 
-Inductive permut [n:Z; A:Set] : (array n A)->(array n A)->Prop :=
-    exchange_is_permut : 
-      (t,t':(array n A))(i,j:Z)(exchange t t' i j) -> (permut t t')
-  | permut_refl : 
-      (t:(array n A))(permut t t)
-  | permut_sym : 
-      (t,t':(array n A))(permut t t') -> (permut t' t)
-  | permut_trans : 
-      (t,t',t'':(array n A))
-      (permut t t') -> (permut t' t'') -> (permut t t'').
+Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop :=
+  | exchange_is_permut :
+      forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t'
+  | permut_refl : forall t:array n A, permut t t
+  | permut_sym : forall t t':array n A, permut t t' -> permut t' t
+  | permut_trans :
+      forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''.
 
-Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datatypes.
+Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62
+  datatypes.
 
 (* We also define the permutation on a segment of an array, "sub_permut",
  * the other parts of the array being unchanged
@@ -47,137 +45,131 @@ Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datat
  * transpositions on the given segment.
  *)
 
-Inductive sub_permut [n:Z; A:Set; g,d:Z] : (array n A)->(array n A)->Prop :=
-    exchange_is_sub_permut : 
-      (t,t':(array n A))(i,j:Z)`g <= i <= d` -> `g <= j <= d`
-      -> (exchange t t' i j) -> (sub_permut g d t t')
-  | sub_permut_refl : 
-      (t:(array n A))(sub_permut g d t t)
-  | sub_permut_sym : 
-      (t,t':(array n A))(sub_permut g d t t') -> (sub_permut g d t' t)
-  | sub_permut_trans : 
-      (t,t',t'':(array n A))
-      (sub_permut g d t t') -> (sub_permut g d t' t'') 
-      -> (sub_permut g d t t'').
-
-Hints Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym sub_permut_trans
-  : v62 datatypes.
+Inductive sub_permut (n:Z) (A:Set) (g d:Z) :
+array n A -> array n A -> Prop :=
+  | exchange_is_sub_permut :
+      forall (t t':array n A) (i j:Z),
+        (g <= i <= d)%Z ->
+        (g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t'
+  | sub_permut_refl : forall t:array n A, sub_permut g d t t
+  | sub_permut_sym :
+      forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t
+  | sub_permut_trans :
+      forall t t' t'':array n A,
+        sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''.
+
+Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym
+  sub_permut_trans: v62 datatypes.
 
 (* To express that some parts of arrays are equal we introduce the
  * property "array_id" which says that a segment is the same on two
  * arrays.
  *)
 
-Definition array_id := [n:Z][A:Set][t,t':(array n A)][g,d:Z]
-  (i:Z) `g <= i <= d` -> #t[i] = #t'[i].
+Definition array_id (n:Z) (A:Set) (t t':array n A) 
+  (g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i].
 
 (* array_id is an equivalence relation *)
 
-Lemma array_id_refl : 
-  (n:Z)(A:Set)(t:(array n A))(g,d:Z)
-  (array_id t t g d).
+Lemma array_id_refl :
+ forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d.
 Proof.
-Unfold array_id.
-Auto with datatypes.
-Save.
+unfold array_id in |- *.
+auto with datatypes.
+Qed.
 
-Hints Resolve array_id_refl : v62 datatypes.
+Hint Resolve array_id_refl: v62 datatypes.
 
 Lemma array_id_sym :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (array_id t t' g d)
-  -> (array_id t' t g d).
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   array_id t t' g d -> array_id t' t g d.
 Proof.
-Unfold array_id. Intros.
-Symmetry; Auto with datatypes.
-Save.
+unfold array_id in |- *. intros.
+symmetry  in |- *; auto with datatypes.
+Qed.
 
-Hints Resolve  array_id_sym : v62 datatypes.
+Hint Resolve array_id_sym: v62 datatypes.
 
 Lemma array_id_trans :
-  (n:Z)(A:Set)(t,t',t'':(array n A))(g,d:Z)
-  (array_id t t' g d)
-  -> (array_id t' t'' g d)
-    -> (array_id t t'' g d).
+ forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z),
+   array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d.
 Proof.
-Unfold array_id. Intros.
-Apply trans_eq with y:=#t'[i]; Auto with datatypes.
-Save.
+unfold array_id in |- *. intros.
+apply trans_eq with (y := #t' [i]); auto with datatypes.
+Qed.
 
-Hints Resolve array_id_trans: v62 datatypes.
+Hint Resolve array_id_trans: v62 datatypes.
 
 (* Outside the segment [g,d] the elements are equal *)
 
 Lemma sub_permut_id :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (array_id t t' `0` `g-1`) /\ (array_id t t' `d+1` `n-1`).
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' ->
+   array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1).
 Proof.
-Intros n A t t' g d. Induction 1; Intros.
-Elim H2; Intros.
-Unfold array_id; Split; Intros.
-Apply H7; Omega.
-Apply H7; Omega.
-Auto with datatypes.
-Decompose [and] H1; Auto with datatypes.
-Decompose [and] H1; Decompose [and] H3; EAuto with datatypes.
-Save.
-
-Hints Resolve sub_permut_id.
+intros n A t t' g d. simple induction 1; intros.
+elim H2; intros.
+unfold array_id in |- *; split; intros.
+apply H7; omega.
+apply H7; omega.
+auto with datatypes.
+decompose [and] H1; auto with datatypes.
+decompose [and] H1; decompose [and] H3; eauto with datatypes.
+Qed.
+
+Hint Resolve sub_permut_id.
 
 Lemma sub_permut_eq :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (i:Z) (`0<=i<g` \/ `d<i<n`) -> #t[i]=#t'[i].
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' ->
+   forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i].
 Proof.
-Intros n A t t' g d Htt' i Hi.
-Elim (sub_permut_id Htt'). Unfold array_id. 
-Intros.
-Elim Hi; [ Intro; Apply H; Omega | Intro; Apply H0; Omega ].
-Save.
+intros n A t t' g d Htt' i Hi.
+elim (sub_permut_id Htt'). unfold array_id in |- *. 
+intros.
+elim Hi; [ intro; apply H; omega | intro; apply H0; omega ].
+Qed.
 
 (* sub_permut is a particular case of permutation *)
 
 Lemma sub_permut_is_permut :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (permut t t').
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' -> permut t t'.
 Proof.
-Intros n A t t' g d. Induction 1; Intros; EAuto with datatypes.
-Save.
+intros n A t t' g d. simple induction 1; intros; eauto with datatypes.
+Qed.
 
-Hints Resolve sub_permut_is_permut.
+Hint Resolve sub_permut_is_permut.
 
 (* If we have a sub-permutation on an empty segment, then we have a 
  * sub-permutation on any segment.
  *)
 
 Lemma sub_permut_void :
-  (N:Z)(A:Set)(t,t':(array N A))
-  (g,g',d,d':Z) `d < g`
-   -> (sub_permut g d t t') -> (sub_permut g' d' t t').
+ forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
+   (d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
 Proof.
-Intros N A t t' g g' d d' Hdg.
-(Induction 1; Intros).
-(Absurd `g <= d`; Omega).
-Auto with datatypes.
-Auto with datatypes.
-EAuto with datatypes.
-Save.
+intros N A t t' g g' d d' Hdg.
+simple induction 1; intros.
+absurd (g <= d)%Z; omega.
+auto with datatypes.
+auto with datatypes.
+eauto with datatypes.
+Qed.
 
 (* A sub-permutation on a segment may be extended to any segment that
  * contains the first one.
  *)
 
 Lemma sub_permut_extension :
-  (N:Z)(A:Set)(t,t':(array N A))
-  (g,g',d,d':Z) `g' <= g` -> `d <= d'`
-   -> (sub_permut g d t t') -> (sub_permut g' d' t t').
+ forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
+   (g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
 Proof.
-Intros N A t t' g g' d d' Hgg' Hdd'.
-(Induction 1; Intros).
-Apply exchange_is_sub_permut with i:=i j:=j; [ Omega | Omega | Assumption ].
-Auto with datatypes.
-Auto with datatypes.
-EAuto with datatypes.
-Save.
+intros N A t t' g g' d d' Hgg' Hdd'.
+simple induction 1; intros.
+apply exchange_is_sub_permut with (i := i) (j := j);
+ [ omega | omega | assumption ].
+auto with datatypes.
+auto with datatypes.
+eauto with datatypes.
+Qed.
\ No newline at end of file
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index 40b19e74f..000a5c913 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -39,37 +39,40 @@ Parameter array : Z -> Set -> Set.
 
 (* Functions to create, access and modify arrays *)
 
-Parameter new : (n:Z)(T:Set) T -> (array n T).
+Parameter new : forall (n:Z) (T:Set), T -> array n T.
 
-Parameter access : (n:Z)(T:Set) (array n T) -> Z -> T.
+Parameter access : forall (n:Z) (T:Set), array n T -> Z -> T.
 
-Parameter store : (n:Z)(T:Set) (array n T) -> Z -> T -> (array n T).
+Parameter store : forall (n:Z) (T:Set), array n T -> Z -> T -> array n T.
 
 
 (* Axioms *)
 
-Axiom new_def : (n:Z)(T:Set)(v0:T)
-                (i:Z) `0<=i<n` -> (access (new n v0) i) = v0.
+Axiom
+  new_def :
+    forall (n:Z) (T:Set) (v0:T) (i:Z),
+      (0 <= i < n)%Z -> access (new n v0) i = v0.
 
-Axiom store_def_1 : (n:Z)(T:Set)(t:(array n T))(v:T)
-                    (i:Z) `0<=i<n` ->
-                    (access (store t i v) i) = v.
+Axiom
+  store_def_1 :
+    forall (n:Z) (T:Set) (t:array n T) (v:T) (i:Z),
+      (0 <= i < n)%Z -> access (store t i v) i = v.
 
-Axiom store_def_2 : (n:Z)(T:Set)(t:(array n T))(v:T)
-                    (i:Z)(j:Z) `0<=i<n` -> `0<=j<n` ->
-		    `i <> j` ->
-                    (access (store t i v) j) = (access t j).
+Axiom
+  store_def_2 :
+    forall (n:Z) (T:Set) (t:array n T) (v:T) (i j:Z),
+      (0 <= i < n)%Z ->
+      (0 <= j < n)%Z -> i <> j -> access (store t i v) j = access t j.
 
-Hints Resolve new_def store_def_1 store_def_2 : datatypes v62.
+Hint Resolve new_def store_def_1 store_def_2: datatypes v62.
 
 (* A tactic to simplify access in arrays *)
 
-Tactic Definition ArrayAccess i j H :=
-    Elim (Z_eq_dec i j); [ 
-      Intro H; Rewrite H; Rewrite store_def_1
-    | Intro H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact H ] ].
+Ltac array_access i j H :=
+  elim (Z_eq_dec i j);
+   [ intro H; rewrite H; rewrite store_def_1
+   | intro H; rewrite store_def_2; [ idtac | idtac | idtac | exact H ] ].
 
 (* Symbolic notation for access *)
 
-Notation "# t [ c ]" := (access t c) (at level 0, t ident)
-  V8only (at level 0, t at level 0).
+Notation "# t [ c ]" := (access t c) (at level 0, t at level 0).
\ No newline at end of file
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index 8f3f90b95..cc36e829f 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -22,4 +22,4 @@ Require Export Arrays.
 
 (*
 Token "'".
-*)
+*)
\ No newline at end of file
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v
index 85c19b48b..8016a2927 100644
--- a/contrib/correctness/Exchange.v
+++ b/contrib/correctness/Exchange.v
@@ -15,80 +15,81 @@
 (*                        Definition and properties                         *)
 (****************************************************************************)
 
-Require ProgInt.
-Require Arrays.
+Require Import ProgInt.
+Require Import Arrays.
 
 Set Implicit Arguments.
 
 (* Definition *)
 
-Inductive exchange [n:Z; A:Set; t,t':(array n A); i,j:Z] : Prop :=
-  exchange_c :
-    `0<=i<n` -> `0<=j<n` ->
-    (#t[i] = #t'[j]) ->
-    (#t[j] = #t'[i]) ->
-    ((k:Z)`0<=k<n` -> `k<>i` -> `k<>j` -> #t[k] = #t'[k]) ->
-    (exchange t t' i j).
+Inductive exchange (n:Z) (A:Set) (t t':array n A) (i j:Z) : Prop :=
+    exchange_c :
+      (0 <= i < n)%Z ->
+      (0 <= j < n)%Z ->
+      #t [i] = #t' [j] ->
+      #t [j] = #t' [i] ->
+      (forall k:Z, (0 <= k < n)%Z -> k <> i -> k <> j -> #t [k] = #t' [k]) ->
+      exchange t t' i j.
     
 (* Properties about exchanges *)
 
-Lemma exchange_1 : (n:Z)(A:Set)(t:(array n A))
-  (i,j:Z) `0<=i<n` -> `0<=j<n` ->
-  (access (store (store t i #t[j]) j #t[i]) i) = #t[j].
+Lemma exchange_1 :
+ forall (n:Z) (A:Set) (t:array n A) (i j:Z),
+   (0 <= i < n)%Z ->
+   (0 <= j < n)%Z -> #(store (store t i #t [j]) j #t [i]) [i] = #t [j].
 Proof.
-Intros n A t i j H_i H_j.
-Case (dec_eq j i).
-Intro eq_i_j. Rewrite eq_i_j.
-Auto with datatypes.
-Intro not_j_i.
-Rewrite (store_def_2 (store t i #t[j]) #t[i] H_j H_i not_j_i).
-Auto with datatypes.
-Save.
+intros n A t i j H_i H_j.
+case (dec_eq j i).
+intro eq_i_j. rewrite eq_i_j.
+auto with datatypes.
+intro not_j_i.
+rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_i not_j_i).
+auto with datatypes.
+Qed.
 
-Hints Resolve exchange_1 : v62 datatypes.
+Hint Resolve exchange_1: v62 datatypes.
 
 
 Lemma exchange_proof :
-  (n:Z)(A:Set)(t:(array n A))
-  (i,j:Z) `0<=i<n` -> `0<=j<n` ->
-  (exchange (store (store t i (access t j)) j (access t i)) t i j).
+ forall (n:Z) (A:Set) (t:array n A) (i j:Z),
+   (0 <= i < n)%Z ->
+   (0 <= j < n)%Z -> exchange (store (store t i #t [j]) j #t [i]) t i j.
 Proof.
-Intros n A t i j H_i H_j.
-Apply exchange_c; Auto with datatypes.
-Intros k H_k not_k_i not_k_j.
-Cut ~j=k; Auto with datatypes. Intro not_j_k.
-Rewrite (store_def_2 (store t i (access t j)) (access t i) H_j H_k not_j_k).
-Auto with datatypes.
-Save.
+intros n A t i j H_i H_j.
+apply exchange_c; auto with datatypes.
+intros k H_k not_k_i not_k_j.
+cut (j <> k); auto with datatypes. intro not_j_k.
+rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_k not_j_k).
+auto with datatypes.
+Qed.
 
-Hints Resolve exchange_proof : v62 datatypes.
+Hint Resolve exchange_proof: v62 datatypes.
 
 
 Lemma exchange_sym :
-  (n:Z)(A:Set)(t,t':(array n A))(i,j:Z)
-  (exchange t t' i j) -> (exchange t' t i j).
+ forall (n:Z) (A:Set) (t t':array n A) (i j:Z),
+   exchange t t' i j -> exchange t' t i j.
 Proof.
-Intros n A t t' i j H1.
-Elim H1. Clear H1. Intros.
-Constructor 1; Auto with datatypes.
-Intros. Rewrite (H3 k); Auto with datatypes.
-Save.
+intros n A t t' i j H1.
+elim H1. clear H1. intros.
+constructor 1; auto with datatypes.
+intros. rewrite (H3 k); auto with datatypes.
+Qed.
 
-Hints Resolve exchange_sym : v62 datatypes.
+Hint Resolve exchange_sym: v62 datatypes.
 
 
 Lemma exchange_id :
-  (n:Z)(A:Set)(t,t':(array n A))(i,j:Z)
-  (exchange t t' i j) -> 
-  i=j ->
-  (k:Z) `0 <= k < n` -> (access t k)=(access t' k).
+ forall (n:Z) (A:Set) (t t':array n A) (i j:Z),
+   exchange t t' i j ->
+   i = j -> forall k:Z, (0 <= k < n)%Z -> #t [k] = #t' [k].
 Proof.
-Intros n A t t' i j Hex Heq k Hk.
-Elim Hex. Clear Hex. Intros.
-Rewrite Heq in H1. Rewrite Heq in H2.
-Case (Z_eq_dec k j). 
-  Intro Heq'. Rewrite Heq'. Assumption.
-  Intro Hnoteq. Apply (H3 k); Auto with datatypes. Rewrite Heq. Assumption.
-Save.
-
-Hints Resolve exchange_id : v62 datatypes.
+intros n A t t' i j Hex Heq k Hk.
+elim Hex. clear Hex. intros.
+rewrite Heq in H1. rewrite Heq in H2.
+case (Z_eq_dec k j). 
+  intro Heq'. rewrite Heq'. assumption.
+  intro Hnoteq. apply (H3 k); auto with datatypes. rewrite Heq. assumption.
+Qed.
+
+Hint Resolve exchange_id: v62 datatypes.
\ No newline at end of file
diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v
index 364cc8d6a..6563fb68a 100644
--- a/contrib/correctness/ProgBool.v
+++ b/contrib/correctness/ProgBool.v
@@ -10,57 +10,57 @@
 
 (* $Id$ *)
 
-Require ZArith.
+Require Import ZArith.
 Require Export Bool_nat.
 Require Export Sumbool.
 
 Definition annot_bool :
-  (b:bool) { b':bool | if b' then b=true else b=false }.
+  forall b:bool, {b' : bool | if b' then b = true else b = false}.
 Proof.
-Intro b.
-Exists b. Case b; Trivial.
-Save.
+intro b.
+exists b. case b; trivial.
+Qed.
 
 
 (* Logical connectives *)
 
-Definition spec_and := [A,B,C,D:Prop][b:bool]if b then A /\ C else B \/ D.
+Definition spec_and (A B C D:Prop) (b:bool) := if b then A /\ C else B \/ D.
 
 Definition prog_bool_and :
-  (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool Q2)
-  -> { b:bool | if b then (Q1 true) /\ (Q2 true)
-                     else (Q1 false) \/ (Q2 false) }.
+  forall Q1 Q2:bool -> Prop,
+    sig Q1 ->
+    sig Q2 ->
+    {b : bool | if b then Q1 true /\ Q2 true else Q1 false \/ Q2 false}.
 Proof.
-Intros Q1 Q2 H1 H2.
-Elim H1. Intro b1. Elim H2. Intro b2. 
-Case b1; Case b2; Intros.
-Exists true; Auto.
-Exists false; Auto. Exists false; Auto. Exists false; Auto.
-Save.
+intros Q1 Q2 H1 H2.
+elim H1. intro b1. elim H2. intro b2. 
+case b1; case b2; intros.
+exists true; auto.
+exists false; auto. exists false; auto. exists false; auto.
+Qed.
 
-Definition spec_or := [A,B,C,D:Prop][b:bool]if b then A \/ C else B /\ D.
+Definition spec_or (A B C D:Prop) (b:bool) := if b then A \/ C else B /\ D.
 
 Definition prog_bool_or :
-  (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool Q2)
-  -> { b:bool | if b then (Q1 true) \/ (Q2 true)
-                     else (Q1 false) /\ (Q2 false) }.
+  forall Q1 Q2:bool -> Prop,
+    sig Q1 ->
+    sig Q2 ->
+    {b : bool | if b then Q1 true \/ Q2 true else Q1 false /\ Q2 false}.
 Proof.
-Intros Q1 Q2 H1 H2.
-Elim H1. Intro b1. Elim H2. Intro b2. 
-Case b1; Case b2; Intros.
-Exists true; Auto. Exists true; Auto. Exists true; Auto.
-Exists false; Auto.
-Save.
+intros Q1 Q2 H1 H2.
+elim H1. intro b1. elim H2. intro b2. 
+case b1; case b2; intros.
+exists true; auto. exists true; auto. exists true; auto.
+exists false; auto.
+Qed.
 
-Definition spec_not:= [A,B:Prop][b:bool]if b then B else A.
+Definition spec_not (A B:Prop) (b:bool) := if b then B else A.
 
 Definition prog_bool_not :
-  (Q:bool->Prop) (sig bool Q)
-  -> { b:bool | if b then (Q false) else (Q true) }.
+  forall Q:bool -> Prop, sig Q -> {b : bool | if b then Q false else Q true}.
 Proof.
-Intros Q H.
-Elim H. Intro b.
-Case b; Intro.
-Exists false; Auto. Exists true; Auto.
-Save.
-
+intros Q H.
+elim H. intro b.
+case b; intro.
+exists false; auto. exists true; auto.
+Qed.
diff --git a/contrib/correctness/ProgInt.v b/contrib/correctness/ProgInt.v
index ec46e2de6..470162ca3 100644
--- a/contrib/correctness/ProgInt.v
+++ b/contrib/correctness/ProgInt.v
@@ -13,7 +13,7 @@
 Require Export ZArith.
 Require Export ZArith_dec.
 
-Theorem Znotzero : (x:Z){`x<>0`}+{`x=0`}.
+Theorem Znotzero : forall x:Z, {x <> 0%Z} + {x = 0%Z}.
 Proof.
-Intro x. Elim (Z_eq_dec x `0`) ; Auto.
-Save.
+intro x. elim (Z_eq_dec x 0); auto.
+Qed.
\ No newline at end of file
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 7e656ae1b..0dafe1010 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -11,188 +11,192 @@
 (* $Id$ *)
 
 Require Export Arrays.
-Require ArrayPermut.
+Require Import ArrayPermut.
 
-Require ZArithRing.
-Require Omega.
-V7only [Import Z_scope.].
+Require Import ZArithRing.
+Require Import Omega.
 Open Local Scope Z_scope.
 
 Set Implicit Arguments.
 
 (* Definition *)
 
-Definition sorted_array :=
-  [N:Z][A:(array N Z)][deb:Z][fin:Z]
-     `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle #A[x] #A[`x+1`]).
+Definition sorted_array (N:Z) (A:array N Z) (deb fin:Z) :=
+  deb <= fin -> forall x:Z, x >= deb -> x < fin -> #A [x] <= #A [x + 1].
 
 (* Elements of a sorted sub-array are in increasing order *)
 
 (* one element and the next one *)
 
 Lemma sorted_elements_1 :
-  (N:Z)(A:(array N Z))(n:Z)(m:Z)
-  (sorted_array A n m)
-  -> (k:Z)`k>=n`
-  -> (i:Z) `0<=i` -> `k+i<=m`
-  -> (Zle (access A k) (access A `k+i`)).
+ forall (N:Z) (A:array N Z) (n m:Z),
+   sorted_array A n m ->
+   forall k:Z,
+     k >= n -> forall i:Z, 0 <= i -> k + i <= m -> #A [k] <= #A [k + i].
 Proof.
-Intros N A n m H_sorted k H_k i H_i.
-Pattern i. Apply natlike_ind.
-Intro.
-Replace `k+0` with k; Omega. (*** Ring `k+0` => BUG ***)
+intros N A n m H_sorted k H_k i H_i.
+pattern i in |- *. apply natlike_ind.
+intro.
+replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***)
 
-Intros.
-Apply Zle_trans with m:=(access A `k+x`).
-Apply H0 ; Omega.
+intros.
+apply Zle_trans with (m := #A [k + x]).
+apply H0; omega.
 
-Unfold Zs.
-Replace `k+(x+1)` with `(k+x)+1`.
-Unfold sorted_array in H_sorted.
-Apply H_sorted ; Omega.
+unfold Zsucc in |- *.
+replace (k + (x + 1)) with (k + x + 1).
+unfold sorted_array in H_sorted.
+apply H_sorted; omega.
 
-Omega.
+omega.
 
-Assumption.
-Save.
+assumption.
+Qed.
 
 (* one element and any of the following *)
 
 Lemma sorted_elements :
-  (N:Z)(A:(array N Z))(n:Z)(m:Z)(k:Z)(l:Z)
-  (sorted_array A n m)
-  -> `k>=n` -> `l<N` -> `k<=l` -> `l<=m`
-  -> (Zle (access A k) (access A l)).
+ forall (N:Z) (A:array N Z) (n m k l:Z),
+   sorted_array A n m ->
+   k >= n -> l < N -> k <= l -> l <= m -> #A [k] <= #A [l].
 Proof.
-Intros.
-Replace l with `k+(l-k)`.
-Apply sorted_elements_1 with n:=n m:=m; [Assumption | Omega | Omega | Omega].
-Omega.
-Save.
+intros.
+replace l with (k + (l - k)).
+apply sorted_elements_1 with (n := n) (m := m);
+ [ assumption | omega | omega | omega ].
+omega.
+Qed.
 
-Hints Resolve sorted_elements : datatypes v62.
+Hint Resolve sorted_elements: datatypes v62.
 
 (* A sub-array of a sorted array is sorted *)
 
-Lemma sub_sorted_array : (N:Z)(A:(array N Z))(deb:Z)(fin:Z)(i:Z)(j:Z)
-      (sorted_array A deb fin) -> 
-        (`i>=deb` -> `j<=fin` -> `i<=j` -> (sorted_array A i j)).
+Lemma sub_sorted_array :
+ forall (N:Z) (A:array N Z) (deb fin i j:Z),
+   sorted_array A deb fin ->
+   i >= deb -> j <= fin -> i <= j -> sorted_array A i j.
 Proof.
-Unfold sorted_array.
-Intros.
-Apply H ; Omega.
-Save.
+unfold sorted_array in |- *.
+intros.
+apply H; omega.
+Qed.
 
-Hints Resolve sub_sorted_array : datatypes v62.
+Hint Resolve sub_sorted_array: datatypes v62.
 
 (* Extension on the left of the property of being sorted *)
 
-Lemma left_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
-   `i>0` -> `j<N` -> (sorted_array A i j) 
-   -> (Zle #A[`i-1`]  #A[i]) -> (sorted_array A `i-1` j).
+Lemma left_extension :
+ forall (N:Z) (A:array N Z) (i j:Z),
+   i > 0 ->
+   j < N ->
+   sorted_array A i j -> #A [i - 1] <= #A [i] -> sorted_array A (i - 1) j.
 Proof.
-(Intros; Unfold sorted_array ; Intros).
-Elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
-Intro Hcut.
-Apply H1 ; Omega.
+intros; unfold sorted_array in |- *; intros.
+elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
+intro Hcut.
+apply H1; omega.
 
-Intro Hcut.
-Replace x with `i-1`.
-Replace `i-1+1` with i ; [Assumption | Omega].
+intro Hcut.
+replace x with (i - 1).
+replace (i - 1 + 1) with i; [ assumption | omega ].
 
-Omega.
-Save.
+omega.
+Qed.
 
 (* Extension on the right *)
 
-Lemma right_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
-   `i>=0` -> `j<N-1` -> (sorted_array A i j) 
-   -> (Zle #A[j]  #A[`j+1`]) -> (sorted_array A i `j+1`).
+Lemma right_extension :
+ forall (N:Z) (A:array N Z) (i j:Z),
+   i >= 0 ->
+   j < N - 1 ->
+   sorted_array A i j -> #A [j] <= #A [j + 1] -> sorted_array A i (j + 1).
 Proof.
-(Intros; Unfold sorted_array ; Intros).
-Elim (Z_lt_ge_dec x j).
-Intro Hcut. 
-Apply H1 ; Omega.
+intros; unfold sorted_array in |- *; intros.
+elim (Z_lt_ge_dec x j).
+intro Hcut. 
+apply H1; omega.
 
-Intro HCut.
-Replace x with j ; [Assumption | Omega].
-Save.
+intro HCut.
+replace x with j; [ assumption | omega ].
+Qed.
 
 (* Substitution of the leftmost value by a smaller value *) 
 
-Lemma left_substitution : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle v #A[i])
-   -> (sorted_array (store A i v) i j).
+Lemma left_substitution :
+ forall (N:Z) (A:array N Z) (i j v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j -> v <= #A [i] -> sorted_array (store A i v) i j.
 Proof.
-Intros N A i j v H_i H_j H_sorted H_v.
-Unfold sorted_array ; Intros.
-
-Cut `x = i`\/`x > i`.
-(Intro Hcut ; Elim Hcut ; Clear Hcut ; Intro).
-Rewrite H2.
-Rewrite store_def_1 ; Try Omega.
-Rewrite store_def_2 ; Try Omega.
-Apply Zle_trans with m:=(access A i) ; [Assumption | Apply H_sorted ; Omega].
-
-(Rewrite store_def_2; Try Omega).
-(Rewrite store_def_2; Try Omega).
-Apply H_sorted ; Omega.
-Omega.
-Save.
+intros N A i j v H_i H_j H_sorted H_v.
+unfold sorted_array in |- *; intros.
+
+cut (x = i \/ x > i).
+intro Hcut; elim Hcut; clear Hcut; intro.
+rewrite H2.
+rewrite store_def_1; try omega.
+rewrite store_def_2; try omega.
+apply Zle_trans with (m := #A [i]); [ assumption | apply H_sorted; omega ].
+
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H_sorted; omega.
+omega.
+Qed.
 
 (* Substitution of the rightmost value by a larger value *)
 
-Lemma right_substitution : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle #A[j] v)
-   -> (sorted_array (store A j v) i j).
+Lemma right_substitution :
+ forall (N:Z) (A:array N Z) (i j v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j -> #A [j] <= v -> sorted_array (store A j v) i j.
 Proof.
-Intros N A i j v H_i H_j H_sorted H_v.
-Unfold sorted_array ; Intros.
-
-Cut `x = j-1`\/`x < j-1`.
-(Intro Hcut ; Elim Hcut ; Clear Hcut ; Intro).
-Rewrite H2.
-Replace `j-1+1` with j; [ Idtac | Omega ]. (*** Ring `j-1+1`. => BUG ***)
-Rewrite store_def_2 ; Try Omega.
-Rewrite store_def_1 ; Try Omega.
-Apply Zle_trans with m:=(access A j). 
-Apply sorted_elements with n:=i m:=j ; Try Omega ; Assumption.
-Assumption.
-
-(Rewrite store_def_2; Try Omega).
-(Rewrite store_def_2; Try Omega).
-Apply H_sorted ; Omega.
-
-Omega.
-Save.
+intros N A i j v H_i H_j H_sorted H_v.
+unfold sorted_array in |- *; intros.
+
+cut (x = j - 1 \/ x < j - 1).
+intro Hcut; elim Hcut; clear Hcut; intro.
+rewrite H2.
+replace (j - 1 + 1) with j; [ idtac | omega ]. (*** Ring `j-1+1`. => BUG ***)
+rewrite store_def_2; try omega.
+rewrite store_def_1; try omega.
+apply Zle_trans with (m := #A [j]). 
+apply sorted_elements with (n := i) (m := j); try omega; assumption.
+assumption.
+
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H_sorted; omega.
+
+omega.
+Qed.
 
 (* Affectation outside of the sorted region *)
 
-Lemma no_effect : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(k:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> `0<=k<i`\/`j<k<N`
-   -> (sorted_array (store A k v) i j).
+Lemma no_effect :
+ forall (N:Z) (A:array N Z) (i j k v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j ->
+   0 <= k < i \/ j < k < N -> sorted_array (store A k v) i j.
 Proof.
-Intros.
-Unfold sorted_array ; Intros. 
-Rewrite store_def_2 ; Try Omega.
-Rewrite store_def_2 ; Try Omega.
-Apply H1 ; Assumption.
-Save.
-
-Lemma sorted_array_id : (N:Z)(t1,t2:(array N Z))(g,d:Z)
-  (sorted_array t1 g d) -> (array_id t1 t2 g d) -> (sorted_array t2 g d).
+intros.
+unfold sorted_array in |- *; intros. 
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H1; assumption.
+Qed.
+
+Lemma sorted_array_id :
+ forall (N:Z) (t1 t2:array N Z) (g d:Z),
+   sorted_array t1 g d -> array_id t1 t2 g d -> sorted_array t2 g d.
 Proof.
-Intros N t1 t2 g d Hsorted Hid.
-Unfold array_id in Hid.
-Unfold sorted_array in Hsorted. Unfold sorted_array.
-Intros Hgd x H1x H2x.
-Rewrite <- (Hid x); [ Idtac | Omega ].
-Rewrite <- (Hid `x+1`); [ Idtac | Omega ].
-Apply Hsorted; Assumption.
-Save.
+intros N t1 t2 g d Hsorted Hid.
+unfold array_id in Hid.
+unfold sorted_array in Hsorted. unfold sorted_array in |- *.
+intros Hgd x H1x H2x.
+rewrite <- (Hid x); [ idtac | omega ].
+rewrite <- (Hid (x + 1)); [ idtac | omega ].
+apply Hsorted; assumption.
+Qed.
\ No newline at end of file
diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v
index f9a3b56b7..41ff10c04 100644
--- a/contrib/correctness/Tuples.v
+++ b/contrib/correctness/Tuples.v
@@ -12,95 +12,87 @@
 
 (* Tuples *)
 
-Definition tuple_1 := [X:Set]X.
+Definition tuple_1 (X:Set) := X.
 Definition tuple_2 := prod.
 Definition Build_tuple_2 := pair.
 Definition proj_2_1 := fst.
 Definition proj_2_2 := snd.
 
-Record tuple_3 [ T1,T2,T3 : Set ] : Set := 
-  { proj_3_1 : T1 ;
-    proj_3_2 : T2 ;
-    proj_3_3 : T3 }.
-
-Record tuple_4 [ T1,T2,T3,T4 : Set ] : Set := 
-  { proj_4_1 : T1 ;
-    proj_4_2 : T2 ;
-    proj_4_3 : T3 ;
-    proj_4_4 : T4 }.
-
-Record tuple_5 [ T1,T2,T3,T4,T5 : Set ] : Set :=
-  { proj_5_1 : T1 ;
-    proj_5_2 : T2 ;
-    proj_5_3 : T3 ;
-    proj_5_4 : T4 ;
-    proj_5_5 : T5 }.
-
-Record tuple_6 [ T1,T2,T3,T4,T5,T6 : Set ] : Set :=
-  { proj_6_1 : T1 ;
-    proj_6_2 : T2 ;
-    proj_6_3 : T3 ;
-    proj_6_4 : T4 ;
-    proj_6_5 : T5 ;
-    proj_6_6 : T6 }.
-
-Record tuple_7 [ T1,T2,T3,T4,T5,T6,T7 : Set ] : Set :=
-  { proj_7_1 : T1 ;
-    proj_7_2 : T2 ;
-    proj_7_3 : T3 ;
-    proj_7_4 : T4 ;
-    proj_7_5 : T5 ;
-    proj_7_6 : T6 ;
-    proj_7_7 : T7 }.
+Record tuple_3 (T1 T2 T3:Set) : Set := 
+  {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}.
 
+Record tuple_4 (T1 T2 T3 T4:Set) : Set := 
+  {proj_4_1 : T1; proj_4_2 : T2; proj_4_3 : T3; proj_4_4 : T4}.
 
-(* Existentials *)
-
-Definition sig_1 := sig.
-Definition exist_1 := exist.
-
-Inductive sig_2 [ T1,T2 : Set; P:T1->T2->Prop ] : Set := 
-  exist_2 : (x1:T1)(x2:T2)(P x1 x2) -> (sig_2 T1 T2 P).
-
-Inductive sig_3 [ T1,T2,T3 : Set; P:T1->T2->T3->Prop ] : Set := 
-  exist_3 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3) -> (sig_3 T1 T2 T3 P).
+Record tuple_5 (T1 T2 T3 T4 T5:Set) : Set := 
+  {proj_5_1 : T1; proj_5_2 : T2; proj_5_3 : T3; proj_5_4 : T4; proj_5_5 : T5}.
 
+Record tuple_6 (T1 T2 T3 T4 T5 T6:Set) : Set := 
+  {proj_6_1 : T1;
+   proj_6_2 : T2;
+   proj_6_3 : T3;
+   proj_6_4 : T4;
+   proj_6_5 : T5;
+   proj_6_6 : T6}.
 
-Inductive sig_4 [ T1,T2,T3,T4 : Set;
-                  P:T1->T2->T3->T4->Prop ] : Set :=
-  exist_4 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)
-             (P x1 x2 x3 x4)
-          -> (sig_4 T1 T2 T3 T4 P).
+Record tuple_7 (T1 T2 T3 T4 T5 T6 T7:Set) : Set := 
+  {proj_7_1 : T1;
+   proj_7_2 : T2;
+   proj_7_3 : T3;
+   proj_7_4 : T4;
+   proj_7_5 : T5;
+   proj_7_6 : T6;
+   proj_7_7 : T7}.
 
-Inductive sig_5 [ T1,T2,T3,T4,T5 : Set;
-                  P:T1->T2->T3->T4->T5->Prop ] : Set :=
-  exist_5 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)
-             (P x1 x2 x3 x4 x5)
-          -> (sig_5 T1 T2 T3 T4 T5 P).
 
-Inductive sig_6 [ T1,T2,T3,T4,T5,T6 : Set;
-                  P:T1->T2->T3->T4->T5->T6->Prop ] : Set :=
-  exist_6 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)
-             (P x1 x2 x3 x4 x5 x6)
-          -> (sig_6 T1 T2 T3 T4 T5 T6 P).
-
-Inductive sig_7 [ T1,T2,T3,T4,T5,T6,T7 : Set;
-                  P:T1->T2->T3->T4->T5->T6->T7->Prop ] : Set :=
-  exist_7 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)(x7:T7)
-             (P x1 x2 x3 x4 x5 x6 x7)
-          -> (sig_7 T1 T2 T3 T4 T5 T6 T7 P).
-
-Inductive sig_8 [ T1,T2,T3,T4,T5,T6,T7,T8 : Set;
-                  P:T1->T2->T3->T4->T5->T6->T7->T8->Prop ] : Set :=
-  exist_8 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)(x7:T7)(x8:T8)
-             (P x1 x2 x3 x4 x5 x6 x7 x8)
-          -> (sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P).      
-
-Inductive dep_tuple_2 [ T1,T2 : Set; P:T1->T2->Set ] : Set := 
-  Build_dep_tuple_2 : (x1:T1)(x2:T2)(P x1 x2) -> (dep_tuple_2 T1 T2 P).
+(* Existentials *)
 
-Inductive dep_tuple_3 [ T1,T2,T3 : Set; P:T1->T2->T3->Set ] : Set := 
-  Build_dep_tuple_3 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3)
-      	       	   -> (dep_tuple_3 T1 T2 T3 P).
+Definition sig_1 := sig.
+Definition exist_1 := exist.
 
+Inductive sig_2 (T1 T2:Set) (P:T1 -> T2 -> Prop) : Set :=
+    exist_2 : forall (x1:T1) (x2:T2), P x1 x2 -> sig_2 T1 T2 P.
+
+Inductive sig_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Prop) : Set :=
+    exist_3 : forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> sig_3 T1 T2 T3 P.
+
+
+Inductive sig_4 (T1 T2 T3 T4:Set) (P:T1 -> T2 -> T3 -> T4 -> Prop) : Set :=
+    exist_4 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4),
+        P x1 x2 x3 x4 -> sig_4 T1 T2 T3 T4 P.
+
+Inductive sig_5 (T1 T2 T3 T4 T5:Set) (P:T1 -> T2 -> T3 -> T4 -> T5 -> Prop) :
+Set :=
+    exist_5 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5),
+        P x1 x2 x3 x4 x5 -> sig_5 T1 T2 T3 T4 T5 P.
+
+Inductive sig_6 (T1 T2 T3 T4 T5 T6:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> Prop) : Set :=
+    exist_6 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6), P x1 x2 x3 x4 x5 x6 -> sig_6 T1 T2 T3 T4 T5 T6 P.
+
+Inductive sig_7 (T1 T2 T3 T4 T5 T6 T7:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> Prop) : Set :=
+    exist_7 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6) (x7:T7),
+        P x1 x2 x3 x4 x5 x6 x7 -> sig_7 T1 T2 T3 T4 T5 T6 T7 P.
+
+Inductive sig_8 (T1 T2 T3 T4 T5 T6 T7 T8:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> T8 -> Prop) : Set :=
+    exist_8 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6) (x7:T7) (x8:T8),
+        P x1 x2 x3 x4 x5 x6 x7 x8 -> sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P.      
+
+Inductive dep_tuple_2 (T1 T2:Set) (P:T1 -> T2 -> Set) : Set :=
+    Build_dep_tuple_2 :
+      forall (x1:T1) (x2:T2), P x1 x2 -> dep_tuple_2 T1 T2 P.
+
+Inductive dep_tuple_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Set) : Set :=
+    Build_dep_tuple_3 :
+      forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> dep_tuple_3 T1 T2 T3 P.