- Procedural: new flag "level=n" to control the reconstruction level (defaults to...

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

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index 958fc4abbd0f80b5db55d89c48872193859260b0..ed30f767b1c9c5175d590d6113cdda4c0d86c691 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -140,15 +140,6 @@ try
    with Not_found -> None
 with Invalid_argument _ -> failwith "A2P.get_inner_types"
 
-let is_proof st v =
-try
-   let id = Ut.id_of_annterm v in
-   try match Hashtbl.find st.sorts id with
-      | `Prop -> true
-      | _     -> false
-   with Not_found -> H.is_proof st.context (H.cic v)
-with Invalid_argument _ -> failwith "P1.is_proof"
-
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -458,48 +449,7 @@ try
 
 with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
-(* object costruction *******************************************************)
-
-let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
-
-let def_flavours = [`Definition; `Variant]
-
-let get_flavour st v attrs =
-   let rec aux = function
-      | []               -> 
-         if is_proof st v then List.hd th_flavours else List.hd def_flavours
-      | `Flavour fl :: _ -> fl
-      | _ :: tl          -> aux tl
-   in
-   let flavour_map x y = match x, y with
-      | None, G.IPAs flavour -> Some flavour
-      | _                    -> x
-   in   
-   match List.fold_left flavour_map None st.params with
-      | Some fl -> fl
-      | None    -> aux attrs
-
-let proc_obj ?(info="") st = function
-   | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
-      begin match get_flavour st v attrs with
-         | flavour when List.mem flavour th_flavours  ->
-            let ast = proc_proof st v in
-            let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
-            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
-              "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
-           in
-            T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
-         | flavour when List.mem flavour def_flavours ->
-            [T.Statement (flavour, Some s, t, Some v, "")]
-        | _                                  ->
-            failwith "not a theorem, definition, axiom or inductive type"
-      end
-   | C.AConstant (_, _, s, None, t, [], attrs)           ->
-      [T.Statement (`Axiom, Some s, t, None, "")]
-   | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
-      [T.Inductive (types, lpsno, "")] 
-   | _                                          ->
-      failwith "not a theorem, definition, axiom or inductive type"
+(* initialization ***********************************************************)
 
 let init ~ids_to_inner_sorts ~ids_to_inner_types params context =
    let depth_map x y = match x, y with