Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.

Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 6dceca87ff375ecadbd8e5d9efcbe6bba044fc52..60c9ab6170e7679e8270dacd106111bff8739be7 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -911,7 +911,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
    prerr_endline ("GB: " ^ NCicPp.ppterm ~metasenv ~subst ~context t
      ^ "        " ^ String.concat "," (List.map (fun i -> NCicPp.ppterm ~metasenv ~subst ~context (C.Rel i)) safes));
  *)
-  match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*)
+  let t = R.whd ~delta:max_int ~subst context t in
+  try
+  match t with
   | C.Rel m as t when List.mem_assoc m recfuns -> 
       raise (NotGuarded (lazy 
         (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
@@ -979,6 +981,13 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
            pl cl
      | _ -> recursor aux k t)
   | t -> recursor aux k t
+  with
+   NotGuarded _ as exc ->
+    let t' = R.whd ~delta:0 ~subst context t in
+     if t = t' then
+      raise exc
+     else
+      aux k t'
  in
   try aux (context, recfuns, 1, []) t
   with NotGuarded s -> raise (TypeCheckerFailure s)