- we replaced a normalize with a whd in the classification algorithm

- we turned on the display of the inner types to debug drop/props.ma

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index ecd4abc744d79704f02a7cd201ba9fcdf295a58e..29b5677312874ccd2ebbf5e1f776261327aeb536 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -58,6 +58,8 @@ type status = {
    skip_thm_and_qed : bool;
 }
 
+let debug = true
+
 (* helpers ******************************************************************)
 
 let split2_last l1 l2 =
@@ -195,24 +197,32 @@ let mk_exp_args hd tl classes synth =
 let mk_convert st ?name sty ety note =
    let e = Cn.hole "" in
    let csty, cety = H.cic sty, H.cic ety in
-   let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
-      note (Pp.ppterm csty) (Pp.ppterm cety)
+   let script = 
+      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 []
    in
    assert (Ut.is_sober csty); 
    assert (Ut.is_sober cety);
-   if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
+   if Ut.alpha_equivalence csty cety then script 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, ""(*note*))]
+      | None         -> T.Change (sty, ety, None, e, "") :: script
       | Some (id, i) -> 
          begin match get_entry st id with
-           | C.Def _  -> assert false (* [T.ClearBody (id, note)] *)
-           | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, "" (* note *))] 
+           | C.Def _  -> assert false (* T.ClearBody (id, "") :: script *)
+           | C.Decl _ -> 
+              T.Change (ety, sty, Some (id, Some id), e, "") :: script 
          end
 
 let convert st ?name v = 
    match get_inner_types st v with
-      | None            -> [(*T.Note "NORMAL: NO INNER TYPES"*)]
+      | None            -> 
+         if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
       | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
 
 let convert_elim st ?name t v pattern =

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index e69b471ca265400e5057f99c5870529c85072e3f..981acc969678302644d591be5bbe540702accd36 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -78,7 +78,7 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_normalize (c, t) in
+   let vs, h = PEH.split_with_whd (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in