From 80f3756848ca8b178255f717794c5c2358d5d585 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 May 2008 22:01:04 +0000 Subject: [PATCH] Partially reverted bad merge by Enrico that re-introduced an un-conditioned whd in guarded_by_destructors. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index ec70116a2..877c33d23 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -731,7 +731,6 @@ and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in let rec aux (context, recfuns, x as k) t = - let t = R.whd ~delta:max_int ~subst context t in (* prerr_endline ("GB:\n" ^ PP.ppcontext ~subst ~metasenv context^ -- 2.39.2