From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 May 2008 22:01:04 +0000 (+0000)
Subject: Partially reverted bad merge by Enrico that re-introduced an un-conditioned
X-Git-Tag: make_still_working~5246
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=80f3756848ca8b178255f717794c5c2358d5d585;p=helm.git

Partially reverted bad merge by Enrico that re-introduced an un-conditioned
whd in guarded_by_destructors.
---

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^