aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppdecl_proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppdecl_proof.ml')
-rw-r--r--parsing/ppdecl_proof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 9e3de9838..ab912cca8 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