- cicUtil: is_sober now detects folded applications

[helm.git] / helm / software / components / acic_procedural / procedural2.ml

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index ed30f767b1c9c5175d590d6113cdda4c0d86c691..dbd70428c7cba8195bc408b4fea6e46889fe3d5a 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -186,28 +186,27 @@ let mk_exp_args hd tl classes synth =
    if args = [] then b, hd else b, C.AAppl ("", hd :: args)
 
 let mk_convert st ?name sty ety note =
+   let ppterm t = 
+      let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a
+   in 
    let e = Cn.hole "" in
    let csty, cety = H.cic sty, H.cic ety in
-   let script = 
+   let note = 
       if !debug then
          let sname = match name with None -> "" | Some (id, _) -> id in
-         let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
-            note sname (Pp.ppterm csty) (Pp.ppterm cety)
-        in 
-        [T.Note note]
-      else []
+         Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
+            note sname (ppterm csty) (ppterm cety)
+      else ""
    in
-   assert (Ut.is_sober st.context csty); 
-   assert (Ut.is_sober st.context cety);
-   if Ut.alpha_equivalence csty cety then script else 
+   if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
-      | None         -> T.Change (sty, ety, None, e, "") :: script
+      | None         -> [T.Change (sty, ety, None, e, note)]
       | Some (id, i) -> 
          begin match get_entry st id with
            | C.Def _  -> assert false (* T.ClearBody (id, "") :: script *)
            | C.Decl _ -> 
-              T.Change (ety, sty, Some (id, Some id), e, "") :: script 
+              [T.Change (ety, sty, Some (id, Some id), e, note)] 
          end
 
 let convert st ?name v =