diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-12 15:56:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-12 15:56:26 +0000 |
| commit | be2ee6dc08ec3cbfb04cdd4b8ecc2b5326805893 (patch) | |
| tree | 31427bd00630c3e9df91d1a1a5384db7e5a3c0a4 /theories7 | |
| parent | 45692339625f409fa1c792a064bfebd553d50a61 (diff) | |
Explicitation d'un nom de variable nécessaire au bon typage, suite à suppression des _ du contexte des evars
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6829 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7')
| -rw-r--r-- | theories7/Logic/Eqdep_dec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories7/Logic/Eqdep_dec.v b/theories7/Logic/Eqdep_dec.v index 81e4bf4f8..6597abfad 100644 --- a/theories7/Logic/Eqdep_dec.v +++ b/theories7/Logic/Eqdep_dec.v @@ -26,10 +26,10 @@ Set Implicit Arguments. (** Bijection between [eq] and [eqT] *) Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y := - [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end. + [A,x,y,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end. Definition eqT2eq: (A:Set)(x,y:A)x==y->x=y := - [A,x,_,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end. + [A,x,y,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end. Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)). Intros. |