X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=63b4d4972281d0c5f5822cf4555ee54b86ff56ee;hb=HEAD;hp=4ce01707cd9d32431f160c1bd28a1f67b6ca05d6;hpb=70660e05baa914569c52555230901d5a8dd92f0b;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 4ce01707c..63b4d4972 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -57,14 +57,23 @@ let get_flavour sorts params context v attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
+let rec is_record = function
+   | []                           -> None
+   | `Class (`Record fields) :: _ -> Some fields
+   | _ :: tl                      -> is_record tl
+
 let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour sorts params context v attrs with
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof 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"
+            let text =
+	       if List.mem G.IPComments params then 
+	          Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+	          "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+	       else
+	          ""
 	    in
             T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
          | flavour when List.mem flavour def_flavours ->
@@ -75,7 +84,10 @@ let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, None, t, [], attrs)           ->
       [T.Statement (`Axiom, Some s, t, None, "")]
    | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
-      [T.Inductive (types, lpsno, "")] 
+      begin match is_record attrs with
+         | None    -> [T.Inductive (types, lpsno, "")]
+	 | Some fs -> [T.Record (types, lpsno, fs, "")]
+      end
    | _                                          ->
       failwith "not a theorem, definition, axiom or inductive type"
 
@@ -130,3 +142,8 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
    in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)
+
+let rec is_debug n = function
+   | []                   -> false
+   | G.IPDebug debug :: _ -> n <= debug
+   | _ :: tl              -> is_debug n tl