X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Fprocedural2.ml;h=7ac82a0a63989326d736864adab9ca2e866d372f;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=ed30f767b1c9c5175d590d6113cdda4c0d86c691;hpb=70660e05baa914569c52555230901d5a8dd92f0b;p=helm.git

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index ed30f767b..7ac82a0a6 100644
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -64,8 +64,8 @@ let debug = ref false
 let split2_last l1 l2 =
 try
    let n = pred (List.length l1) in
-   let before1, after1 = HEL.split_nth n l1 in
-   let before2, after2 = HEL.split_nth n l2 in
+   let before1, after1 = HEL.split_nth "P2 1" n l1 in
+   let before2, after2 = HEL.split_nth "P2 2" n l2 in
    before1, before2, List.hd after1, List.hd after2
 with Invalid_argument _ -> failwith "A2P.split2_last"
    
@@ -186,28 +186,30 @@ 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.Def _  -> 
+	       [T.Change (ety, sty, Some (id, Some id), e, note);
+	        T.ClearBody (id, "")
+	       ]
 	    | 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 = 
@@ -279,8 +281,10 @@ and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
-      let st, hyp, rqv = match get_inner_types st v with
-         | Some (ity, _) ->
+      let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
+         | Some (C.ALetIn _, _), _ ->
+	    st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
+	 | _, Some (ity, _)        ->
 	    let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl ->
 	          mk_fwd_rewrite st dtext intro tl true v t ity
@@ -293,7 +297,7 @@ and proc_letin st what name v w t =
 		  st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
 	    in
 	    st, C.Decl (H.cic ity), rqv
-	 | None          ->
+	 | _, None                 ->
 	    st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
@@ -384,7 +388,7 @@ and proc_case st what uri tyno u v ts =
       let qs = proc_bkd_proofs (next st) synth names classes ts in
       let lpsno, _ = H.get_ind_type uri tyno in
       let ps, _ = H.get_ind_parameters st.context (H.cic v) in
-      let _, rps = HEL.split_nth lpsno ps in
+      let _, rps = HEL.split_nth "P2 3" lpsno ps in
       let rpsno = List.length rps in 
       let e = Cn.mk_pattern rpsno u in
       let text = "" in