diff options
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | parsing/printer.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 8b9c59b117..765e55b37c 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -230,7 +230,7 @@ let print_one_inductive (sp,tyi) = let env = Global.env () in let envpar = push_rel_context params env in hov 0 ( - pr_global (IndRef (sp,tyi)) ++ brk(1,2) ++ print_params env params ++ + pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++ str ": " ++ prterm_env envpar arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar cstrnames cstrtypes diff --git a/parsing/printer.ml b/parsing/printer.ml index fbae23c2d9..2a64ed8eda 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -155,15 +155,15 @@ let pr_var_decl env (id,c,typ) = let pr_rel_decl env (na,c,typ) = let pbody = match c with - | None -> (mt ()) + | None -> mt () | Some c -> (* Force evaluation *) let pb = prterm_env env c in (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = prtype_env env typ in match na with - | Anonymous -> (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - | Name id -> (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) (* Prints out an "env" in a nice format. We print out the @@ -190,7 +190,7 @@ let pr_rel_context env rel_context = else (str "(" ++ pb ++ str")" ++ spc () ++ penvtl) in - prec env (List.rev rel_context) + hov 0 (prec env (List.rev rel_context)) (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env = |