diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-13 10:41:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-13 10:41:29 +0000 |
| commit | a8f20849f28494dee5bd23458168747525eba8d0 (patch) | |
| tree | 66853fe3d516ec896c764cdbfe9b912c2b72ea74 /parsing | |
| parent | 077502620d56a33604b9dfaf0a214516e0d780a2 (diff) | |
Ameliration affichage inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4615 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 8b9c59b11..765e55b37 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 fbae23c2d..2a64ed8ed 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 = |