cicDischarge: new module for discharging the explicit variables occurring in a

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 380e52efec280ca40f308a92b5e0bcafd00c2998..deb3088f22537b32e368a03b54de920e8776a488 100644 (file)
--- 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