diff options
| author | filliatr | 1999-12-12 22:04:30 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-12 22:04:30 +0000 |
| commit | 0579791aa362fbed66baff317cb29f204dcce18a (patch) | |
| tree | b792a03fdc9a333b72bad0d663e60279c545e986 /parsing/printer.ml | |
| parent | ed8ec17ce48b4d0cf14696a4e9760239aa31f59b (diff) | |
modules et coqc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@239 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index df0daa1301..fcda9fb93e 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -33,9 +33,10 @@ let with_implicits f x = Termast.print_implicits := oimpl; raise e let pr_qualified sp id = - if Nametab.sp_of_id (kind_of_path sp) id = sp - then [< 'sTR(string_of_id id) >] - else [< 'sTR(string_of_path sp) >] + if Nametab.sp_of_id (kind_of_path sp) id = sp then + [< 'sTR(string_of_id id) >] + else + [< 'sTR(string_of_path sp) >] let pr_constant sp = pr_qualified sp (basename sp) @@ -205,7 +206,7 @@ let dbenv_it_with f env e = (* Prints a signature, all declarations on the same line if possible *) let pr_sign sign = hV 0 [< (sign_it_with (fun id t sign pps -> - [< pps ; 'wS 2 ; print_decl CCI sign (id,t) >]) + [< pps; 'wS 2; print_decl CCI sign (id,t) >]) sign) [< >] >] (* Prints an env (variables and de Bruijn). Separator: newline *) @@ -213,13 +214,13 @@ let pr_env k env = let sign_env = sign_it_with (fun id t sign pps -> - let pidt = print_decl k sign (id,t) in [< pps ; 'fNL ; pidt >]) + let pidt = print_decl k sign (id,t) in [< pps; 'fNL; pidt >]) (get_globals env) [< >] in let db_env = dbenv_it_with (fun na t env pps -> - let pnat = print_binding k env (na,t) in [< pps ; 'fNL ; pnat >]) + let pnat = print_binding k env (na,t) in [< pps; 'fNL; pnat >]) env [< >] in [< sign_env; db_env >] @@ -251,7 +252,7 @@ let pr_env_limit n env = dbenv_it_with (fun na t env pps -> let pnat = print_binding CCI env (na,t) in - [< pps ; 'fNL ; + [< pps; 'fNL; 'sTR (emacs_str (String.make 1 (Char.chr 253))); pnat >]) env [< >] |