Merge branch 'experimental/upstream' into upstream

4 files changed, 30 insertions, 36 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 26c8ef59..779c3d9a 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Operators_Properties.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (************************************************************************)
 (** * Some properties of the operators on relations                     *)
 (************************************************************************)
@@ -19,17 +17,17 @@ Require Import Relation_Operators.
 
 Section Properties.
 
-  Implicit Arguments clos_refl_trans [A].
-  Implicit Arguments clos_refl_trans_1n [A].
-  Implicit Arguments clos_refl_trans_n1 [A].
-  Implicit Arguments clos_refl_sym_trans [A].
-  Implicit Arguments clos_refl_sym_trans_1n [A].
-  Implicit Arguments clos_refl_sym_trans_n1 [A].
-  Implicit Arguments clos_trans [A].
-  Implicit Arguments clos_trans_1n [A].
-  Implicit Arguments clos_trans_n1 [A].
-  Implicit Arguments inclusion [A].
-  Implicit Arguments preorder [A].
+  Arguments clos_refl_trans [A] R x _.
+  Arguments clos_refl_trans_1n [A] R x _.
+  Arguments clos_refl_trans_n1 [A] R x _.
+  Arguments clos_refl_sym_trans [A] R _ _.
+  Arguments clos_refl_sym_trans_1n [A] R x _.
+  Arguments clos_refl_sym_trans_n1 [A] R x _.
+  Arguments clos_trans [A] R x _.
+  Arguments clos_trans_1n [A] R x _.
+  Arguments clos_trans_n1 [A] R x _.
+  Arguments inclusion [A] R1 R2.
+  Arguments preorder [A] R.
 
   Variable A : Type.
   Variable R : relation A.
@@ -52,7 +50,7 @@ Section Properties.
 
     Lemma clos_rt_idempotent : inclusion (R*)* R*.
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       intros.
       apply rt_trans with y; auto with sets.
@@ -68,7 +66,7 @@ Section Properties.
     Lemma clos_rt_clos_rst :
       inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
@@ -89,7 +87,7 @@ Section Properties.
       inclusion (clos_refl_sym_trans (clos_refl_sym_trans R))
       (clos_refl_sym_trans R).
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 0d901445..0e6d034e 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relation_Definitions.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Section Relation_Definition.
 
   Variable A : Type.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 6efebc46..b7159578 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -1,25 +1,25 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relation_Operators.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (************************************************************************)
-(** *                   Bruno Barras, Cristina Cornes                   *)
+(** * Some operators on relations                                       *)
+(************************************************************************)
+(** * Initial authors: Bruno Barras, Cristina Cornes                    *)
 (** *                                                                   *)
-(** * Some of these definitions were taken from :                       *)
+(** * Some of the initial definitions were taken from :                 *)
 (** *    Constructing Recursion Operators in Type Theory                *)
 (** *    L. Paulson  JSC (1986) 2, 325-355                              *)
+(** *                                                                   *)
+(** * Further extensions by Pierre Castéran                             *)
 (************************************************************************)
 
 Require Import Relation_Definitions.
 
-(** * Some operators to build relations *)
-
 (** ** Transitive closure *)
 
 Section Transitive_Closure.
@@ -149,13 +149,13 @@ Section Lexicographic_Product.
   Variable leA : A -> A -> Prop.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
-  Inductive lexprod : sigS B -> sigS B -> Prop :=
+  Inductive lexprod : sigT B -> sigT B -> Prop :=
     | left_lex :
       forall (x x':A) (y:B x) (y':B x'),
-        leA x x' -> lexprod (existS B x y) (existS B x' y')
+        leA x x' -> lexprod (existT B x y) (existT B x' y')
     | right_lex :
       forall (x:A) (y y':B x),
-        leB x y y' -> lexprod (existS B x y) (existS B x y').
+        leB x y y' -> lexprod (existT B x y) (existT B x y').
 
 End Lexicographic_Product.
 
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 630b2822..08b7574f 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relations.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relation_Definitions.
 Require Export Relation_Operators.
 Require Export Operators_Properties.
@@ -16,16 +14,16 @@ Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
-  intros; split; elim H; red in |- *; auto.
+  intros; split; elim H; red; auto.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
-  split; red in |- *;
+  split; red;
     [  (* reflexivity *) reflexivity
       |  (* transitivity *) intros; transitivity (f y); assumption
-      |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+      |  (* symmetry *) intros; symmetry ; assumption ].
 Qed.