- some depend files fixed

[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 2fec2dd1f9b2bb996c5a2e26a3bdd7552fbeed29..63b4d4972281d0c5f5822cf4555ee54b86ff56ee 100644 (file)
--- 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"