| `Theorem -> "Theorem"
let pp_command = function
- | Abort -> "Abort."
- | Check term -> sprintf "Check %s." (CicAstPp.pp_term term)
- | Proof -> "Proof."
+ | Abort -> "Abort"
+ | Check term -> sprintf "Check %s" (CicAstPp.pp_term term)
+ | Proof -> "Proof"
| Qed name ->
- (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
- | Quit -> "Quit."
+ (match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
+ | Quit -> "Quit"
| Theorem (flavour, name, typ, body) ->
- sprintf "%s %s: %s %s."
+ sprintf "%s %s: %s %s"
(pp_flavour flavour)
(match name with None -> "" | Some name -> name)
(CicAstPp.pp_term typ)