cicUtil : new test function "is_sober" to test the integrity of a term

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index f39aa18bd96ee3a162baa10fa6da07ca3b6f8805..cc4ec10a340e9793999d5b09bbd3d12b4dcd40c8 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -198,6 +198,8 @@ let mk_convert st ?name sty ety note =
    let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
       note (Pp.ppterm csty) (Pp.ppterm cety)
    in
+   assert (Ut.is_sober csty); 
+   assert (Ut.is_sober cety);
    if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
    match name with
       | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
@@ -266,7 +268,7 @@ let mk_rewrite st dtext where qs tl direction t =
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
-      | None          -> true
+      | None          -> false
       | Some (it, et) -> 
          DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in