+module H = HExtlib
+module C = Content
+module G = GrafiteAst
+
+(* grafite ast constructors *************************************************)
+
+let floc = H.dummy_floc
+
+let mk_note str = G.Comment (floc, G.Note (floc, str))
+
+(* interface functions ******************************************************)
+
+let out_arg = function
+ | C.Aux _ -> "aux"
+ | C.Premise _ -> "premise"
+ | C.Lemma _ -> "lemma"
+ | C.Term _ -> "term"
+ | C.ArgProof _ -> "proof"
+ | C.ArgMethod _ -> "method"
+
+let out_args args = String.concat " " (List.map out_arg args)
+
+let out_name = function
+ | None -> ""
+ | Some str -> str
+
+let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) =
+ if List.length params > 0 || xmenv <> None then assert false;
+ match obj with
+ | `Def (C.Const, t, `Proof {
+ C.proof_name = Some name; C.proof_context = [];
+ C.proof_apply_context = []; C.proof_conclude = {
+ C.conclude_conclusion = Some b
+ }
+ }) ->
+ [mk_note (Printf.sprintf "%s" name)]
+ | _ -> assert false