diff options
| author | filliatr | 2001-05-28 12:14:49 +0000 |
|---|---|---|
| committer | filliatr | 2001-05-28 12:14:49 +0000 |
| commit | 6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b (patch) | |
| tree | 4a33333de304fb331f0f7b2b9ea761a8301b2f8d /toplevel | |
| parent | 47bde1826b6329650f8546ac1fca1f2e90d85fcb (diff) | |
Pretty -> Prettyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
2 files changed, 5 insertions, 6 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e9194d8a85..d044232b6c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -22,7 +22,6 @@ open Type_errors open Reduction open Cases open Logic -open Pretty open Printer open Ast diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d684633b8..1010ec1c38 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -27,7 +27,7 @@ open Vernacinterp open Coqast open Ast open Astterm -open Pretty +open Prettyp open Printer open Tacinterp open Tactic_debug @@ -1383,26 +1383,26 @@ let _ = let _ = add "PrintGRAPH" (function - | [] -> (fun () -> pPNL (Pretty.print_graph())) + | [] -> (fun () -> pPNL (Prettyp.print_graph())) | _ -> bad_vernac_args "PrintGRAPH") let _ = add "PrintCLASSES" (function - | [] -> (fun () -> pPNL (Pretty.print_classes())) + | [] -> (fun () -> pPNL (Prettyp.print_classes())) | _ -> bad_vernac_args "PrintCLASSES") let _ = add "PrintCOERCIONS" (function - | [] -> (fun () -> pPNL (Pretty.print_coercions())) + | [] -> (fun () -> pPNL (Prettyp.print_coercions())) | _ -> bad_vernac_args "PrintCOERCIONS") let _ = add "PrintPATH" (function | [VARG_IDENTIFIER ids;VARG_IDENTIFIER idt] -> - (fun () -> pPNL (Pretty.print_path_between ids idt)) + (fun () -> pPNL (Prettyp.print_path_between ids idt)) | _ -> bad_vernac_args "PrintPATH") (* Meta-syntax commands *) |