From be2ee6dc08ec3cbfb04cdd4b8ecc2b5326805893 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Mar 2005 15:56:26 +0000
Subject: 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
---
 theories7/Logic/Eqdep_dec.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories7/Logic/Eqdep_dec.v b/theories7/Logic/Eqdep_dec.v
index 81e4bf4f8a..6597abfad6 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.
-- 
cgit v1.2.3