From 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 07:42:16 +0100 Subject: [api] Miscellaneous consolidation + moves to engine. We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. --- library/lib.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 36292d367..6abbf7ef9 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -12,7 +12,7 @@ open Util open Names open Libnames open Globnames -open Nameops +(* open Nameops *) open Libobject open Context.Named.Declaration @@ -361,8 +361,8 @@ let end_compilation_checks dir = | None -> anomaly (Pp.str "There should be a module name...") | Some m -> if not (Names.DirPath.equal m dir) then anomaly - (str "The current open module has name" ++ spc () ++ pr_dirpath m ++ - spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str "."); + (str "The current open module has name" ++ spc () ++ DirPath.print m ++ + spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); in oname -- cgit v1.2.3