JMeq maintenant applicable sur Type

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

1 files changed, 21 insertions, 12 deletions

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 3b07322d6..96bab3dc7 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -19,56 +19,65 @@
 
 Set Implicit Arguments.
 
-Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop :=
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
     JMeq_refl : JMeq x x.
-Reset JMeq_ind.
+Reset JMeq_rect.
 
 Hint Resolve JMeq_refl.
 
-Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x.
+Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
 destruct 1; trivial.
 Qed.
 
 Hint Immediate sym_JMeq.
 
 Lemma trans_JMeq :
- forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
+ forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
 destruct 1; trivial.
 Qed.
 
-Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y.
+Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
 
-Lemma JMeq_ind : forall (A:Set) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
+Lemma JMeq_ind : forall (A:Type) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
 intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rec : forall (A:Set) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
+Lemma JMeq_rec : forall (A:Type) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
+intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Qed.
+
+Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
 intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
 Lemma JMeq_ind_r :
- forall (A:Set) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
+ forall (A:Type) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
 intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
 Lemma JMeq_rec_r :
- forall (A:Set) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
+ forall (A:Type) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
+intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Qed.
+
+Lemma JMeq_rect_r :
+ forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
 intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
-(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *)
+(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *)
 
 Require Import Eqdep.
 
 Lemma JMeq_eq_dep :
- forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y.
+ forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
 Proof.
 destruct 1.
 apply eq_dep_intro.
 Qed.
 
 Lemma eq_dep_JMeq :
- forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y.
+ forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
 Proof.
 destruct 1.
 apply JMeq_refl.