dummy dependent types and dummy letins are now removed from the refined

[helm.git] / helm / gTopLevel / tests / lambda02.cic.test

diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test
index ee8c6b118e11f287ec0e91ea28095faa0b837be6..fde5288f91a4e5e35ad0eb899ee1809d8e8e5232 100644 (file)
--- a/helm/gTopLevel/tests/lambda02.cic.test
+++ b/helm/gTopLevel/tests/lambda02.cic.test
@@ -2,8 +2,8 @@
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
-[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
+[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))
 ### (* TYPE_OF the disambiguated term *)
-(f:(n:nat)(H:(le O n))(eq nat n n))(eq nat O O)
+(f:(n:nat)((le O n)->(eq nat n n)))(eq nat O O)
 ### (* REDUCED disambiguated term     *)
-[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
+[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))