X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=b37eef6bbc989034b8dbe2e7fd851dc454baf943;hb=3b8d99d5fdb79a5d979a8e200a4a4307fe362009;hp=c004fd346b4e2a9ff30714fa3cf84af50a5acf00;hpb=6ba374cbb94797e58cd997c5b41099dd9f679a57;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index c004fd346..b37eef6bb 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -167,7 +167,7 @@ let get_entry st id =
 
 let get_ind_names uri tno =
 try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
+   let ts = match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (ts, _, _, _), _ -> ts 
       | _                                      -> assert false
    in
@@ -347,20 +347,24 @@ and proc_appl st what hd tl =
       let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
-	    let classes, tl, _, where = split2_last classes tl in
-	    let script = List.rev (mk_arg st where) @ script in
-	    let synth = I.S.add 1 synth in
+	    let classes2, tl2, _, where = split2_last classes tl in
+	    let script2 = List.rev (mk_arg st where) @ script in
+	    let synth2 = I.S.add 1 synth in
 	    let names = get_ind_names uri tyno in
-	    let qs = proc_bkd_proofs (next st) synth names classes tl in
-            if is_rewrite_right hd then 
-	       script @ mk_rewrite st dtext where qs tl false what
+	    let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+            if List.length qs <> List.length names then
+	       let qs = proc_bkd_proofs (next st) synth [] classes tl in
+	       let hd = mk_exp_args hd tl classes synth in
+	       script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+	    else if is_rewrite_right hd then 
+	       script2 @ mk_rewrite st dtext where qs tl2 false what
 	    else if is_rewrite_left hd then 
-	       script @ mk_rewrite st dtext where qs tl true what
+	       script2 @ mk_rewrite st dtext where qs tl2 true what
 	    else
-	       let predicate = List.nth tl (parsno - i) in
+	       let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
 	       let using = Some hd in
-	       (* convert_elim st what what e @ *) script @ 
+	       (* convert_elim st what what e @ *) script2 @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let qs = proc_bkd_proofs (next st) synth [] classes tl in