diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-02 15:49:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-02 15:49:21 +0000 |
| commit | 0bf91ea32d8fe2e0a6e9464950d6e7d66eadaf6b (patch) | |
| tree | 27549c07d703f97c041696cd2e6563cad21ab32e /theories/Logic/Eqdep_dec.v | |
| parent | 7b7bbdda56f2697c6bc721bb645278cf225f9ee9 (diff) | |
eq2eqT et eqT2eq devenus obsolètes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5794 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 22476505f..e3c336344 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -25,7 +25,7 @@ Set Implicit Arguments. (** Bijection between [eq] and [eqT] *) - Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : + Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : x = y := match eqxy in (_ = y) return x = y with | refl_equal => refl_equal x @@ -146,8 +146,7 @@ End DecidableEqDep. (forall x y:A, {x = y} + {x <> y}) -> forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. intros. -rewrite eq_eqT_bij. -elim (eq2eqT p) using K_dec. +elim p using K_dec. intros. case (H x0 y); intros. elim e; left; reflexivity. @@ -155,4 +154,4 @@ elim e; left; reflexivity. right; red in |- *; intro neq; apply n; elim neq; reflexivity. trivial. -Qed.
\ No newline at end of file +Qed. |