Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à

égalité décidable + maj dépendances


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

1 files changed, 21 insertions, 11 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 03d29db35..8123d8d85 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -535,21 +535,31 @@ Definition PeanoView_iter (P:positive->Type)
   | PeanoSucc _ q => f _ (iter _ q)
   end).
 
-Require Import JMeq.
+Require Import Eqdep_dec EqdepFacts.
+
+Theorem eq_dep_eq_positive :
+  forall (P:positive->Type) (p:positive) (x y:P p), 
+  eq_dep positive P p x p y -> x = y.
+Proof.
+apply eq_dep_eq_dec.
+decide equality.
+Qed.
 
 Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.  
 Proof.
 intros. 
-induction q. apply JMeq_eq. cut (xH=xH). pattern xH at 1 2 5, q'. destruct q'. trivial.
-destruct p0; intros; discriminate.
-trivial.
-apply JMeq_eq.
-cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
-intro. destruct p; discriminate.
-intro. unfold p0 in H. apply Psucc_inj in H.
-generalize q'. rewrite H. intro.
-rewrite (IHq q'0).
-trivial.
+induction q. 
+apply eq_dep_eq_positive. 
+  cut (xH=xH). pattern xH at 1 2 5, q'. destruct q'. trivial.
+  destruct p0; intros; discriminate.
+  trivial.
+apply eq_dep_eq_positive.
+  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
+  intro. destruct p; discriminate.
+  intro. unfold p0 in H. apply Psucc_inj in H.
+  generalize q'. rewrite H. intro.
+  rewrite (IHq q'0).
+  trivial.
 trivial.
 Qed.