diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/prettyp.ml | 9 | ||||
| -rw-r--r-- | printing/printer.ml | 1 |
3 files changed, 7 insertions, 9 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 143f9ddcc5..e897b19387 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -447,7 +447,7 @@ open Decl_kinds | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt pr_dirpath dir + keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> keyword "Print Modules" | PrintMLLoadPath -> @@ -518,7 +518,7 @@ open Decl_kinds in keyword cmd ++ spc() ++ pr_smart_global qid | PrintNamespace dp -> - keyword "Print Namespace" ++ pr_dirpath dp + keyword "Print Namespace" ++ DirPath.print dp | PrintStrategy None -> keyword "Print Strategies" | PrintStrategy (Some qid) -> @@ -964,7 +964,7 @@ open Decl_kinds keyword "LoadPath" ++ spc() ++ qs s ++ (match d with | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir)) + | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) ) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e2d23ce7b0..8fc00ed96d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Termops open Declarations open Environ @@ -139,7 +138,7 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in - let ctx = prod_assum typ in + let ctx = Term.prod_assum typ in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -366,7 +365,7 @@ let pr_located_qualid = function | DirModule (dir,_) -> "Module", dir | DirClosedSection dir -> "Closed Section", dir in - str s ++ spc () ++ pr_dirpath dir + str s ++ spc () ++ DirPath.print dir | ModuleType mp -> str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) | Other (obj, info) -> info.name obj @@ -490,7 +489,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = let print_named_def env sigma name body typ = let pbody = pr_lconstr_env env sigma body in let ptyp = pr_ltype_env env sigma typ in - let pbody = if isCast body then surround pbody else pbody in + let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ @@ -647,7 +646,7 @@ let gallina_print_library_entry env sigma with_values ent = | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> - Some (str " >>>>>>> Library " ++ pr_dirpath dir) + Some (str " >>>>>>> Library " ++ DirPath.print dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> diff --git a/printing/printer.ml b/printing/printer.ml index 377a6b4e12..d7bb0460d5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Term open Constr open Environ open Globnames |