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

3 files changed, 286 insertions, 267 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 31e3ac447d..95a40ab12d 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -12,103 +12,102 @@
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
-Require Sorting.
+Require Import List.
+Require Import Multiset.
+Require Import Permutation.
+Require Import Relations.
+Require Import Sorting.
 
 
 Section defs.
 
 Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
+Variable leA : relation A.
+Variable eqA : relation A.
 
-Local gtA := [x,y:A]~(leA x y).
+Let gtA (x y:A) := ~ leA x y.
 
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
+Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
 
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
 
 Inductive Tree : Set :=
-      Tree_Leaf : Tree
-    | Tree_Node : A -> Tree -> Tree -> Tree.
+  | Tree_Leaf : Tree
+  | Tree_Node : A -> Tree -> Tree -> Tree.
 
 (** [a] is lower than a Tree [T] if [T] is a Leaf
     or [T] is a Node holding [b>a] *)
 
-Definition leA_Tree := [a:A; t:Tree]
- Cases t of 
-   Tree_Leaf           => True
- | (Tree_Node b T1 T2) => (leA a b)
- end.
+Definition leA_Tree (a:A) (t:Tree) :=
+  match t with
+  | Tree_Leaf => True
+  | Tree_Node b T1 T2 => leA a b
+  end.
 
-Lemma leA_Tree_Leaf : (a:A)(leA_Tree a Tree_Leaf).
+Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
 Proof.
-Simpl; Auto with datatypes.
+simpl in |- *; auto with datatypes.
 Qed.
 
-Lemma leA_Tree_Node : (a,b:A)(G,D:Tree)(leA a b) ->
-                        (leA_Tree a (Tree_Node b G D)).
+Lemma leA_Tree_Node :
+ forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
 Proof.
-Simpl; Auto with datatypes.
+simpl in |- *; auto with datatypes.
 Qed.
 
-Hints Resolve leA_Tree_Leaf leA_Tree_Node.
+Hint Resolve leA_Tree_Leaf leA_Tree_Node.
 
 
 (** The heap property *)
 
 Inductive is_heap : Tree -> Prop :=
-      nil_is_heap : (is_heap Tree_Leaf)
-    | node_is_heap : (a:A)(T1,T2:Tree)
-                     (leA_Tree a T1) ->
-                     (leA_Tree a T2) ->
-                     (is_heap T1) -> (is_heap T2) ->
-                     (is_heap (Tree_Node a T1 T2)).
-
-Hint constr_is_heap := Constructors is_heap.
-
-Lemma invert_heap : (a:A)(T1,T2:Tree)(is_heap (Tree_Node a T1 T2))->
-  (leA_Tree a T1) /\ (leA_Tree a T2) /\
-  (is_heap T1) /\ (is_heap T2).
+  | nil_is_heap : is_heap Tree_Leaf
+  | node_is_heap :
+      forall (a:A) (T1 T2:Tree),
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
+
+Hint Constructors is_heap.
+
+Lemma invert_heap :
+ forall (a:A) (T1 T2:Tree),
+   is_heap (Tree_Node a T1 T2) ->
+   leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
 Proof.
-Intros; Inversion H; Auto with datatypes.
+intros; inversion H; auto with datatypes.
 Qed.
 
 (* This lemma ought to be generated automatically by the Inversion tools *)
-Lemma is_heap_rec : (P:Tree->Set)
-        (P Tree_Leaf)->
-         ((a:A)
-           (T1:Tree)
-            (T2:Tree)
-             (leA_Tree a T1)->
-              (leA_Tree a T2)->
-               (is_heap T1)->
-                (P T1)->(is_heap T2)->(P T2)->(P (Tree_Node a T1 T2)))
-         -> (T:Tree)(is_heap T) -> (P T).
+Lemma is_heap_rec :
+ forall P:Tree -> Set,
+   P Tree_Leaf ->
+   (forall (a:A) (T1 T2:Tree),
+      leA_Tree a T1 ->
+      leA_Tree a T2 ->
+      is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+   forall T:Tree, is_heap T -> P T.
 Proof.
-Induction T; Auto with datatypes.
-Intros a G PG D PD PN. 
-Elim (invert_heap a G D); Auto with datatypes.
-Intros H1 H2; Elim H2; Intros H3 H4; Elim H4; Intros.
-Apply H0; Auto with datatypes.
+simple induction T; auto with datatypes.
+intros a G PG D PD PN. 
+elim (invert_heap a G D); auto with datatypes.
+intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+apply H0; auto with datatypes.
 Qed.
 
-Lemma low_trans : 
-  (T:Tree)(a,b:A)(leA a b) -> (leA_Tree b T) -> (leA_Tree a T).
+Lemma low_trans :
+ forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
 Proof.
-Induction T; Auto with datatypes.
-Intros; Simpl; Apply leA_trans with b; Auto with datatypes.
+simple induction T; auto with datatypes.
+intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
 Qed.
 
 (** contents of a tree as a multiset *)
@@ -117,107 +116,112 @@ Qed.
     in not used. Actually, we could just take as postulate:
     [Parameter SingletonBag : A->multiset].  *)
 
-Fixpoint  contents [t:Tree] : (multiset A) :=
- Cases t of
-   Tree_Leaf           => emptyBag
- | (Tree_Node a t1 t2) => (munion (contents t1) 
-                          (munion (contents t2) (singletonBag a)))
-end.
+Fixpoint contents (t:Tree) : multiset A :=
+  match t with
+  | Tree_Leaf => emptyBag
+  | Tree_Node a t1 t2 =>
+      munion (contents t1) (munion (contents t2) (singletonBag a))
+  end.
 
 
 (** equivalence of two trees is equality of corresponding multisets *)
 
-Definition equiv_Tree := [t1,t2:Tree](meq (contents t1) (contents t2)).
+Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
 
 
 (** specification of heap insertion *)
 
-Inductive insert_spec [a:A; T:Tree] : Set :=
-   insert_exist : (T1:Tree)(is_heap T1) ->
-                  (meq (contents T1) (munion (contents T) (singletonBag a))) ->
-                  ((b:A)(leA b a)->(leA_Tree b T)->(leA_Tree b T1)) ->
-                  (insert_spec a T).
+Inductive insert_spec (a:A) (T:Tree) : Set :=
+    insert_exist :
+      forall T1:Tree,
+        is_heap T1 ->
+        meq (contents T1) (munion (contents T) (singletonBag a)) ->
+        (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+        insert_spec a T.
 
 
-Lemma insert : (T:Tree)(is_heap T) -> (a:A)(insert_spec a T).
+Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
 Proof.
-Induction 1; Intros.
-Apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); Auto with datatypes.
-Simpl; Unfold meq munion; Auto with datatypes.
-Elim (leA_dec a a0); Intros.
-Elim (H3 a0); Intros.
-Apply insert_exist with (Tree_Node a T2 T0); Auto with datatypes.
-Simpl; Apply treesort_twist1; Trivial with datatypes. 
-Elim (H3 a); Intros T3 HeapT3 ConT3 LeA.
-Apply insert_exist with (Tree_Node a0 T2 T3); Auto with datatypes.
-Apply node_is_heap; Auto with datatypes.
-Apply low_trans with a; Auto with datatypes.
-Apply LeA; Auto with datatypes.
-Apply low_trans with a; Auto with datatypes.
-Simpl; Apply treesort_twist2; Trivial with datatypes. 
+simple induction 1; intros.
+apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+ auto with datatypes.
+simpl in |- *; unfold meq, munion in |- *; auto with datatypes.
+elim (leA_dec a a0); intros.
+elim (H3 a0); intros.
+apply insert_exist with (Tree_Node a T2 T0); auto with datatypes.
+simpl in |- *; apply treesort_twist1; trivial with datatypes. 
+elim (H3 a); intros T3 HeapT3 ConT3 LeA.
+apply insert_exist with (Tree_Node a0 T2 T3); auto with datatypes.
+apply node_is_heap; auto with datatypes.
+apply low_trans with a; auto with datatypes.
+apply LeA; auto with datatypes.
+apply low_trans with a; auto with datatypes.
+simpl in |- *; apply treesort_twist2; trivial with datatypes. 
 Qed.
 
 (** building a heap from a list *)
 
-Inductive build_heap [l:(list A)] : Set :=
-   heap_exist : (T:Tree)(is_heap T) ->
-                (meq (list_contents eqA_dec l)(contents T)) ->
-                (build_heap l).
+Inductive build_heap (l:list A) : Set :=
+    heap_exist :
+      forall T:Tree,
+        is_heap T ->
+        meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
 
-Lemma list_to_heap : (l:(list A))(build_heap l).
+Lemma list_to_heap : forall l:list A, build_heap l.
 Proof.
-Induction l.
-Apply (heap_exist (nil  A) Tree_Leaf); Auto with datatypes.
-Simpl; Unfold meq; Auto with datatypes.
-Induction 1.
-Intros T i m; Elim (insert T i a).
-Intros; Apply heap_exist with T1; Simpl; Auto with datatypes.
-Apply meq_trans with (munion (contents T) (singletonBag a)).
-Apply meq_trans with (munion (singletonBag a) (contents T)).
-Apply meq_right; Trivial with datatypes.
-Apply munion_comm.
-Apply meq_sym; Trivial with datatypes.
+simple induction l.
+apply (heap_exist nil Tree_Leaf); auto with datatypes.
+simpl in |- *; unfold meq in |- *; auto with datatypes.
+simple induction 1.
+intros T i m; elim (insert T i a).
+intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
+apply meq_trans with (munion (contents T) (singletonBag a)).
+apply meq_trans with (munion (singletonBag a) (contents T)).
+apply meq_right; trivial with datatypes.
+apply munion_comm.
+apply meq_sym; trivial with datatypes.
 Qed.
 
 
 (** building the sorted list *)
 
-Inductive flat_spec [T:Tree] : Set :=
- flat_exist : (l:(list A))(sort leA l) ->
-              ((a:A)(leA_Tree a T)->(lelistA leA a l)) ->
-              (meq (contents T) (list_contents eqA_dec l)) ->
-              (flat_spec T).
+Inductive flat_spec (T:Tree) : Set :=
+    flat_exist :
+      forall l:list A,
+        sort leA l ->
+        (forall a:A, leA_Tree a T -> lelistA leA a l) ->
+        meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
 
-Lemma heap_to_list : (T:Tree)(is_heap T) -> (flat_spec T).
+Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
 Proof.
-  Intros T h; Elim h; Intros.
-  Apply flat_exist with (nil A); Auto with datatypes.
-  Elim H2; Intros l1 s1 i1 m1; Elim H4; Intros l2 s2 i2 m2.
-  Elim (merge leA_dec eqA_dec s1 s2); Intros.
-  Apply flat_exist with (cons a l); Simpl; Auto with datatypes.
-  Apply meq_trans with 
-    (munion (list_contents eqA_dec l1) (munion (list_contents eqA_dec l2) 
-                                               (singletonBag a))).
-  Apply meq_congr; Auto with datatypes.
-  Apply meq_trans with 
-    (munion (singletonBag a) (munion (list_contents eqA_dec l1) 
-                                     (list_contents eqA_dec  l2))).
-  Apply munion_rotate.
-  Apply meq_right; Apply meq_sym; Trivial with datatypes.
+  intros T h; elim h; intros.
+  apply flat_exist with (nil (A:=A)); auto with datatypes.
+  elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
+  elim (merge _ leA_dec eqA_dec s1 s2); intros.
+  apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (list_contents _ eqA_dec l1)
+      (munion (list_contents _ eqA_dec l2) (singletonBag a))).
+  apply meq_congr; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+  apply munion_rotate.
+  apply meq_right; apply meq_sym; trivial with datatypes.
 Qed.
 
 (** specification of treesort *)
 
-Theorem treesort : (l:(list A))
-  {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}.
+Theorem treesort :
+ forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
 Proof.
-  Intro l; Unfold permutation.
-  Elim (list_to_heap l).
-  Intros.
-  Elim (heap_to_list T); Auto with datatypes.
-  Intros.
-  Exists l0; Auto with datatypes.
-  Apply meq_trans with (contents T); Trivial with datatypes.
+  intro l; unfold permutation in |- *.
+  elim (list_to_heap l).
+  intros.
+  elim (heap_to_list T); auto with datatypes.
+  intros.
+  exists l0; auto with datatypes.
+  apply meq_trans with (contents T); trivial with datatypes.
 Qed.
 
-End defs.
+End defs.
\ No newline at end of file
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 3702387a7f..bfb42b7b9e 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,104 +8,113 @@
 
 (*i $Id$ i*)
 
-Require Relations.
-Require PolyList.
-Require Multiset.
+Require Import Relations.
+Require Import List.
+Require Import Multiset.
 
 Set Implicit Arguments.
 
 Section defs.
 
 Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
+Variable leA : relation A.
+Variable eqA : relation A.
 
-Local gtA := [x,y:A]~(leA x y).
+Let gtA (x y:A) := ~ leA x y.
 
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{~(leA x y)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
+Hypothesis leA_dec : forall x y:A, {leA x y} + {~ leA x y}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
-Hints Resolve leA_refl : default.
-Hints Immediate eqA_dec leA_dec leA_antisym : default.
+Hint Resolve leA_refl: default.
+Hint Immediate eqA_dec leA_dec leA_antisym: default.
 
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
 
 (** contents of a list *)
 
-Fixpoint list_contents [l:(list A)] : (multiset A) :=
- Cases l of
-   nil        => emptyBag
- | (cons a l) => (munion (singletonBag a) (list_contents l))
- end.
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | nil => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
 
-Lemma list_contents_app : (l,m:(list A))
-  (meq (list_contents (app l m)) (munion (list_contents l) (list_contents m))).
+Lemma list_contents_app :
+ forall l m:list A,
+   meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
 Proof.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with  
- (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); Auto with datatypes.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+ auto with datatypes.
 Qed.
-Hints Resolve list_contents_app.
+Hint Resolve list_contents_app.
 
-Definition permutation := [l,m:(list A)](meq (list_contents l) (list_contents m)).
+Definition permutation (l m:list A) :=
+  meq (list_contents l) (list_contents m).
 
-Lemma permut_refl : (l:(list A))(permutation l l).
+Lemma permut_refl : forall l:list A, permutation l l.
 Proof.
-Unfold permutation; Auto with datatypes.
+unfold permutation in |- *; auto with datatypes.
 Qed.
-Hints Resolve permut_refl.
+Hint Resolve permut_refl.
 
-Lemma permut_tran : (l,m,n:(list A))
-   (permutation l m) -> (permutation m n) -> (permutation l n).
+Lemma permut_tran :
+ forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
 Proof.
-Unfold permutation; Intros.
-Apply meq_trans with (list_contents m); Auto with datatypes.
+unfold permutation in |- *; intros.
+apply meq_trans with (list_contents m); auto with datatypes.
 Qed.
 
-Lemma permut_right : (l,m:(list A))
-   (permutation l m) -> (a:A)(permutation (cons a l) (cons a m)).
+Lemma permut_right :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
 Proof.
-Unfold permutation; Simpl; Auto with datatypes.
+unfold permutation in |- *; simpl in |- *; auto with datatypes.
 Qed.
-Hints Resolve permut_right.
+Hint Resolve permut_right.
 
-Lemma permut_app : (l,l',m,m':(list A))
-   (permutation l l') -> (permutation m m') ->
-   (permutation (app l m) (app l' m')).
+Lemma permut_app :
+ forall l l' m m':list A,
+   permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
 Proof.
-Unfold permutation; Intros.
-Apply meq_trans with (munion (list_contents l) (list_contents m)); Auto with datatypes.
-Apply meq_trans with (munion (list_contents l') (list_contents m')); Auto with datatypes.
-Apply meq_trans with (munion (list_contents l') (list_contents m)); Auto with datatypes.
+unfold permutation in |- *; intros.
+apply meq_trans with (munion (list_contents l) (list_contents m));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m'));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m));
+ auto with datatypes.
 Qed.
-Hints Resolve permut_app.
+Hint Resolve permut_app.
 
-Lemma permut_cons : (l,m:(list A))(permutation l m) ->
-    (a:A)(permutation (cons a l) (cons a m)).
+Lemma permut_cons :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
 Proof.
-Intros l m H a.
-Change (permutation (app (cons a (nil A)) l) (app (cons a (nil A)) m)).
-Apply permut_app; Auto with datatypes.
+intros l m H a.
+change (permutation ((a :: nil) ++ l) ((a :: nil) ++ m)) in |- *.
+apply permut_app; auto with datatypes.
 Qed.
-Hints Resolve permut_cons.
+Hint Resolve permut_cons.
 
-Lemma permut_middle : (l,m:(list A))
-   (a:A)(permutation (cons a (app l m)) (app l (cons a m))).
+Lemma permut_middle :
+ forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
 Proof.
-Unfold permutation.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with (munion (singletonBag a)
-          (munion (singletonBag a0) (list_contents (app l0 m)))); Auto with datatypes.
-Apply munion_perm_left; Auto with datatypes.
+unfold permutation in |- *.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a)
+    (munion (singletonBag a0) (list_contents (l0 ++ m))));
+ auto with datatypes.
+apply munion_perm_left; auto with datatypes.
 Qed.
-Hints Resolve permut_middle.
+Hint Resolve permut_middle.
 
 End defs.
 Unset Implicit Arguments.
-
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index cad4e20198..b1986d4e74 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -8,110 +8,116 @@
 
 (*i $Id$ i*)
 
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
+Require Import List.
+Require Import Multiset.
+Require Import Permutation.
+Require Import Relations.
 
 Set Implicit Arguments.
 
 Section defs.
 
 Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
+Variable leA : relation A.
+Variable eqA : relation A.
 
-Local gtA := [x,y:A]~(leA x y).
+Let gtA (x y:A) := ~ leA x y.
 
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
+Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
 
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
 
 (** [lelistA] *)
 
-Inductive lelistA [a:A] : (list A) -> Prop :=
-      nil_leA : (lelistA a (nil A))
-    | cons_leA : (b:A)(l:(list A))(leA a b)->(lelistA a (cons b l)).
-Hint constr_lelistA := Constructors lelistA.
+Inductive lelistA (a:A) : list A -> Prop :=
+  | nil_leA : lelistA a nil
+  | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
+Hint Constructors lelistA.
 
-Lemma lelistA_inv : (a,b:A)(l:(list A))
-      (lelistA a (cons b l)) -> (leA a b).
+Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
 Proof.
-  Intros; Inversion H; Trivial with datatypes.
+  intros; inversion H; trivial with datatypes.
 Qed.
 
 (** definition for a list to be sorted *)
 
-Inductive sort : (list A) -> Prop :=
-   nil_sort : (sort (nil A))
- | cons_sort : (a:A)(l:(list A))(sort l) -> (lelistA a l) -> (sort (cons a l)).
-Hint constr_sort := Constructors sort.
+Inductive sort : list A -> Prop :=
+  | nil_sort : sort nil
+  | cons_sort :
+      forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l).
+Hint Constructors sort.
 
-Lemma sort_inv : (a:A)(l:(list A))(sort (cons a l))->(sort l) /\ (lelistA a l).
+Lemma sort_inv :
+ forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
 Proof.
-Intros; Inversion H; Auto with datatypes.
+intros; inversion H; auto with datatypes.
 Qed.
 
-Lemma sort_rec : (P:(list A)->Set)
-     (P (nil A)) ->
-     ((a:A)(l:(list A))(sort l)->(P l)->(lelistA a l)->(P (cons a l))) ->
-     (y:(list A))(sort y) -> (P y).
+Lemma sort_rec :
+ forall P:list A -> Set,
+   P nil ->
+   (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
+   forall y:list A, sort y -> P y.
 Proof.
-Induction y; Auto with datatypes.
-Intros; Elim (!sort_inv a l); Auto with datatypes.
+simple induction y; auto with datatypes.
+intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
 Qed.
 
 (** merging two sorted lists *)
 
-Inductive merge_lem [l1:(list A);l2:(list A)] : Set :=
-  merge_exist : (l:(list A))(sort l) ->
-    (meq (list_contents eqA_dec l)
-         (munion (list_contents eqA_dec l1) (list_contents eqA_dec l2))) ->
-    ((a:A)(lelistA a l1)->(lelistA a l2)->(lelistA a l)) ->
-    (merge_lem l1 l2).
-
-Lemma merge : (l1:(list A))(sort l1)->(l2:(list A))(sort l2)->(merge_lem l1 l2).
+Inductive merge_lem (l1 l2:list A) : Set :=
+    merge_exist :
+      forall l:list A,
+        sort l ->
+        meq (list_contents _ eqA_dec l)
+          (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+        (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->
+        merge_lem l1 l2.
+
+Lemma merge :
+ forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2.
 Proof.
-  Induction 1; Intros.
-  Apply merge_exist with l2; Auto with datatypes.
-  Elim H3; Intros.
-  Apply merge_exist with (cons a l); Simpl; Auto with datatypes.
-  Elim (leA_dec a a0); Intros.
+  simple induction 1; intros.
+  apply merge_exist with l2; auto with datatypes.
+  elim H3; intros.
+  apply merge_exist with (a :: l); simpl in |- *; auto with datatypes.
+  elim (leA_dec a a0); intros.
 
 (* 1 (leA a a0) *)
-  Cut (merge_lem l (cons a0 l0)); Auto with datatypes.
-  Intros (l3, l3sorted, l3contents, Hrec).
-  Apply merge_exist with (cons a l3); Simpl; Auto with datatypes.
-  Apply meq_trans with (munion (singletonBag a)
-	                       (munion (list_contents eqA_dec l)
-                                       (list_contents eqA_dec (cons a0 l0)))).
-  Apply meq_right; Trivial with datatypes.
-  Apply meq_sym; Apply munion_ass.
-  Intros; Apply cons_leA.
-  Apply lelistA_inv with l; Trivial with datatypes.
+  cut (merge_lem l (a0 :: l0)); auto with datatypes.
+  intros [l3 l3sorted l3contents Hrec].
+  apply merge_exist with (a :: l3); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a)
+      (munion (list_contents _ eqA_dec l)
+         (list_contents _ eqA_dec (a0 :: l0)))).
+  apply meq_right; trivial with datatypes.
+  apply meq_sym; apply munion_ass.
+  intros; apply cons_leA.
+  apply lelistA_inv with l; trivial with datatypes.
 
 (* 2 (leA a0 a) *)
-  Elim H5; Simpl; Intros.
-  Apply merge_exist with (cons a0 l3); Simpl; Auto with datatypes.
-  Apply meq_trans with (munion (singletonBag a0)
-                               (munion (munion (singletonBag a) 
-                                               (list_contents eqA_dec l))
-                               (list_contents eqA_dec l0))).
-  Apply meq_right; Trivial with datatypes.
-  Apply munion_perm_left.
-  Intros; Apply cons_leA; Apply lelistA_inv with l0; Trivial with datatypes.
+  elim H5; simpl in |- *; intros.
+  apply merge_exist with (a0 :: l3); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a0)
+      (munion (munion (singletonBag a) (list_contents _ eqA_dec l))
+         (list_contents _ eqA_dec l0))).
+  apply meq_right; trivial with datatypes.
+  apply munion_perm_left.
+  intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes.
 Qed.
 
 End defs.
 
 Unset Implicit Arguments.
-Hint constr_sort : datatypes v62 := Constructors sort.
-Hint constr_lelistA : datatypes v62 := Constructors lelistA.
+Hint Constructors sort: datatypes v62.
+Hint Constructors lelistA: datatypes v62.
\ No newline at end of file