+let pp_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Goal -> "Goal"
+ | `Lemma -> "Lemma"
+ | `Remark -> "Remark"
+ | `Theorem -> "Theorem"
+
+let pp_search_kind = function
+ | `Locate -> "locate"
+ | `Hint -> "hint"
+ | `Match -> "match"
+ | `Elim -> "elim"
+
+let pp_command = function
+ | Abort -> "Abort"
+ | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
+ | Baseuri None -> "Baseuri"
+ | Check term -> sprintf "Check %s" (pp_term term)
+ | Proof -> "Proof"
+ | Qed name ->
+ (match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
+ | Quit -> "Quit"
+ | Redo None -> "Redo"
+ | Redo (Some n) -> sprintf "Redo %d" n
+ | Search_pat (kind, pat) ->
+ sprintf "search %s \"%s\"" (pp_search_kind kind) pat
+ | Search_term (kind, term) ->
+ sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
+ | Inductive (params, types) ->
+ let pp_params = function
+ | [] -> ""
+ | params ->
+ " " ^
+ String.concat " "
+ (List.map
+ (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
+ params)
+ in
+ let pp_constructors constructors =
+ String.concat "\n"
+ (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
+ constructors)
+ in
+ let pp_type (name, _, typ, constructors) =
+ sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
+ (pp_constructors constructors)
+ in
+ (match types with
+ | [] -> assert false
+ | (name, inductive, typ, constructors) :: tl ->
+ let fst_typ_pp =
+ sprintf "%sinductive %s%s: %s \\def\n%s"
+ (if inductive then "" else "co") name (pp_params params)
+ (pp_term typ) (pp_constructors constructors)
+ in
+ fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Theorem (flavour, name, typ, body) ->
+ sprintf "%s %s: %s %s"
+ (pp_flavour flavour)
+ (match name with None -> "" | Some name -> name)
+ (pp_term typ)
+ (match body with
+ | None -> ""
+ | Some body -> "\\def " ^ pp_term body)
+ | Undo None -> "Undo"
+ | Undo (Some n) -> sprintf "Undo %d" n
+