diff options
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 *) |