From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 Apr 2008 17:52:04 +0000 (+0000)
Subject: Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
X-Git-Tag: make_still_working~5283
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fbadb3454a52d879edc58a4a09ca46c1e77dce2f;p=helm.git

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 6dceca87f..60c9ab617 100644
--- 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)