From c408e819ce39b27f0842c84b1b24c585ac5b6086 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 01:14:50 +0100 Subject: [lib] [api] Introduce record for `object_prefix` This is a minor cleanup adding a record in a try to structure the state living in `Lib`. --- printing/printmod.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing/printmod.ml') diff --git a/printing/printmod.ml b/printing/printmod.ml index 13a03e9b4..dd2e99d58 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -237,10 +237,10 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn -let nametab_register_dir mp = +let nametab_register_dir obj_mp = let id = mk_fake_top () in - let dir = DirPath.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + let obj_dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here -- cgit v1.2.3