+let pp_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Goal -> "Goal"
+ | `Lemma -> "Lemma"
+ | `Remark -> "Remark"
+ | `Theorem -> "Theorem"
+
+let pp_command = function
+ | Proof -> "Proof."
+ | Theorem (flavour, name, typ, body) ->
+ sprintf "%s %s: %s %s."
+ (pp_flavour flavour)
+ (match name with None -> "" | Some name -> name)
+ (CicAstPp.pp_term typ)
+ (match body with
+ | None -> ""
+ | Some body -> "\\def " ^ CicAstPp.pp_term body)
+ | Qed name ->
+ (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
+ | Quit -> "Quit."
+