diff options
| author | coq | 2002-08-13 14:44:24 +0000 |
|---|---|---|
| committer | coq | 2002-08-13 14:44:24 +0000 |
| commit | a3848b0a10064fb7e206a503ac8b829cb9ce4666 (patch) | |
| tree | 57715eb46564f71b91825c46ecb432a41c1ec095 /dev | |
| parent | bc4e7b8c2317b2536eb42efb7cbf37d748ceb7c6 (diff) | |
Petites corrections ici et la
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0339a8fddd..62fc841e6f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -34,7 +34,8 @@ let prast c = pp(print_ast c) let prastpat c = pp(print_astpat c) let prastpatl c = pp(print_astlpat c) -let ppterm = (fun x -> pp(prterm x)) +let ppterm x = pp(prterm x) +let ppterm_univ x = Termast.with_universes ppterm x let pprawterm = (fun x -> pp(pr_rawterm x)) let pppattern = (fun x -> pp(pr_pattern x)) let pptype = (fun x -> pp(prtype x)) |