From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 library/libobject.mli | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'library/libobject.mli')

diff --git a/library/libobject.mli b/library/libobject.mli
index 9e41b7fa..09938189 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -1,12 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Libnames
 open Mod_subst
 
@@ -45,7 +44,9 @@ open Mod_subst
 
    * a substitution function, performing the substitution;
      this function should be declared for substitutive objects
-     only (see above)
+     only (see above). NB: the substitution might now be delayed
+     instead of happening at module creation, so this function
+     should _not_ depend on the current environment
 
    * a discharge function, that is applied at section closing time to
      collect the data necessary to rebuild the discharged form of the
@@ -98,6 +99,7 @@ val declare_object :
   'a object_declaration -> ('a -> obj)
 
 val object_tag : obj -> string
+val object_has_tag : obj -> string -> bool
 
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
-- 
cgit v1.2.3