X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=deb3088f22537b32e368a03b54de920e8776a488;hb=04f22df647f35080b499b720bca7bc0eb1794c64;hp=380e52efec280ca40f308a92b5e0bcafd00c2998;hpb=9e03c0de729a0c42cfdd55a2cee085a59f7632a8;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 380e52efe..deb3088f2 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -146,12 +146,6 @@ try
    with Not_found -> `Type (CicUniv.fresh())
 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.oblivion_ugraph in
-   ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -160,16 +154,6 @@ let get_entry st id =
    in
    aux st.context
 
-let get_ind_names uri tno =
-try   
-   let ts = match E.get_obj Un.oblivion_ugraph uri with
-      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
-      | _                                      -> assert false
-   in
-   match List.nth ts tno with
-      | (_, _, _, cs) -> List.map fst cs  
-with Invalid_argument _ -> failwith "A2P.get_ind_names"
-
 let string_of_atomic = function
    | C.ARel (_, _, _, s)               -> s
    | C.AVar (_, uri, _)                -> H.name_of_uri uri None None
@@ -187,6 +171,8 @@ let get_sub_names head l =
    let names, _ = List.fold_left map ([], 1) l in 
    List.rev names
 
+let get_type msg st t = H.get_type msg st.context (H.cic t) 
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "PREMISE"
@@ -378,7 +364,7 @@ and proc_appl st what hd tl =
 	    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 names = H.get_ind_names uri tyno in
 	    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