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. --- kernel/names.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index cb27104d1..b02c0b840 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -179,6 +179,8 @@ struct | [] -> "<>" | sl -> String.concat "." (List.rev_map Id.to_string sl) + let print dp = str (to_string dp) + let initial = [default_module_name] module Hdir = Hashcons.Hlist(Id) -- cgit v1.2.3