| 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
| 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"
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