X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=63b4d4972281d0c5f5822cf4555ee54b86ff56ee;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=9152d7a436234d68eb7bb29776ed7e5b21268af0;hpb=14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 9152d7a43..63b4d4972 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -57,6 +57,11 @@ 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
@@ -79,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"
 
@@ -137,5 +145,5 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
 
 let rec is_debug n = function
    | []                   -> false
-   | G.IPDebug debug :: _ -> debug <= n
+   | G.IPDebug debug :: _ -> n <= debug
    | _ :: tl              -> is_debug n tl