- | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
- ^ NotationPp.pp_term status term ^ "such that" ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
- | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
- NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
- ^ " (" ^ ident2 ^ ")"
- | Thesisbecomes (_, t) -> "the thesis becomes" ^ NotationPp.pp_term status t
- | RewritingStep (_, rhs, just, cont) ->
- "=" ^
- NotationPp.pp_term status rhs ^
- (match just with
- | `Auto params -> pp_auto_params params status
- | `Term t -> " exact " ^ NotationPp.pp_term status t
+ | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": ("
+ ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")"
+ | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^
+ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status
+ term2)
+ ^ ") (" ^ ident2 ^ ")"
+ | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")"
+ | RewritingStep (_, rhs, just, cont) ->
+ "= (" ^
+ (NotationPp.pp_term status rhs) ^ ")" ^
+ (match just with
+ | `Auto params -> let s = pp_auto_params params status in
+ if s <> "" then " by " ^ s
+ else ""
+ | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")"