diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppdecl_proof.ml | 2 | ||||
| -rw-r--r-- | parsing/tactic_printer.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index 9e3de9838b..ab912cca88 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -155,7 +155,7 @@ let rec pr_bare_proof_instr _then _thus env = function | Pcast (id,typ) -> str "reconsider" ++ spc () ++ pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ (pr_constr env typ) + str "as" ++ spc () ++ (pr_constr env typ) | Psuppose hyps -> str "suppose" ++ print_hyps pr_constr _I env false false "we have" hyps diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index b0e487ac5f..91c1bc0c4f 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -189,7 +189,7 @@ let print_treescript nochange sigma pf = | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - hv indent (pr_rule_dot r ++ prlist_with_sep fnl aux spfl) + hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl) in hov 0 (aux pf) let rec print_info_script sigma osign pf = |