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 ec70116a211d6594149d2abe0b7ca36fb9e5a25f..877c33d23edf73c5c09a5c274afd1cfe60898564 100644 (file)
--- 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^