From a03648b7ed6bc8159b3fed9aa0a21b0cecfbea2f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Feb 2004 16:18:15 +0000 Subject: [PATCH] New implementation of eat_prods. Some residual problems disappear. --- helm/gTopLevel/tests/lambda03.cic.test | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/gTopLevel/tests/lambda03.cic.test b/helm/gTopLevel/tests/lambda03.cic.test index 558be3839..e6d731cde 100644 --- a/helm/gTopLevel/tests/lambda03.cic.test +++ b/helm/gTopLevel/tests/lambda03.cic.test @@ -1,8 +1,7 @@ \lambda n:nat. \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H)) ### (* METASENV after disambiguation *) - |- ?4: Type -n : nat; H : (eq nat n n) |- ?5: ?4[] + ### (* TERM after disambiguation *) [n:nat][H:(eq nat n n)][g:(((x:nat)((eq nat x x)->(le x O))->(le n O))->True)](g [f:(x:nat)((eq nat x x)->(le x O))](f n H)) ### (* TYPE_OF the disambiguated term *) -- 2.39.2