From dccaed2452e544308b46f0c73ffd4f542ef4c8c6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 26 Oct 2018 10:24:18 +0200
Subject: [libobject] Move object_name next to object definition.

`object_name` is a particular choice of the implementation of
`Liboject`, thus it makes sense to tie it to that particular module.

This may prove useful in the future as we may want to modify object
naming.
---
 interp/declare.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.mli b/interp/declare.mli
index 02e73cd66c..468e056909 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Libnames
 open Constr
 open Entries
 open Decl_kinds
@@ -29,7 +28,7 @@ type section_variable_entry =
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
-val declare_variable : variable -> variable_declaration -> object_name
+val declare_variable : variable -> variable_declaration -> Libobject.object_name
 
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
@@ -69,7 +68,7 @@ val set_declare_scheme :
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> object_name * bool
+val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
 
 (** Declaration messages *)
 
-- 
cgit v1.2.3