X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=f39aa18bd96ee3a162baa10fa6da07ca3b6f8805;hb=55ec3926f6fbb5dba13705659fe94d0db38b2666;hp=9815580b6444ef8bb31669e0fd60aaae5cebb60b;hpb=797f61edb93f41eb2c5e281bc9457f6bff633063;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 9815580b6..f39aa18bd 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -54,7 +54,8 @@ type status = {
    intros: string option list;
    clears: string list;
    clears_note: string;
-   case: int list
+   case: int list;
+   skip_thm_and_qed : bool;
 }
 
 (* helpers ******************************************************************)
@@ -249,7 +250,7 @@ let mk_fwd_rewrite st dtext name tl direction t =
    match where with
       | C.ARel (_, _, i, premise) as v ->
          let where = Some (premise, name) in
-         let _script = convert_elim st ~name:(premise, i) t v e in 
+(*         let _script = convert_elim st ~name:(premise, i) t v e in *) 
          let script = mk_arg st what @ mk_arg st v (* @ script *) in
 	 let st = {st with context = Cn.clear st.context premise} in 
 	 st, T.Rewrite (direction, what, where, e, dtext) :: script
@@ -259,7 +260,7 @@ let mk_rewrite st dtext where qs tl direction t =
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
-   let script = convert_elim st t t e in
+   let script = [] (* convert_elim st t t e *) in
    script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
@@ -350,7 +351,7 @@ and proc_appl st what hd tl =
 	       let predicate = List.nth tl (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 @ *) script @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let qs = proc_bkd_proofs (next st) synth [] classes tl in
@@ -376,7 +377,7 @@ and proc_proof st t =
       in
       let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       let note = Pp.ppcontext st.context ^ note in
-      {st with context = context; clears = clears; clears_note = note}
+      {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
       | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
@@ -422,13 +423,15 @@ let proc_obj st = function
       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 "tactics: %u\nnodes: %u" steps nodes in
-      T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
+      if st.skip_thm_and_qed then ast
+      else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 
 (* interface functions ******************************************************)
 
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = 
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+?(skip_thm_and_qed=false) prefix aobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -439,7 +442,8 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       intros      = [];
       clears      = [];
       clears_note = "";
-      case        = []
+      case        = [];
+      skip_thm_and_qed = skip_thm_and_qed;
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in