From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 library/global.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index 72429c76..ab70bb7c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Term
@@ -121,16 +119,22 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
-let constant_of_delta con = 
+let constant_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO : are resolver and resolver_param orthogonal ?
+     the effect of resolver is lost if resolver_param isn't
+     trivial at that spot. *)
     Mod_subst.constant_of_delta resolver_param
-      (Mod_subst.constant_of_delta resolver con)
+      (Mod_subst.constant_of_delta_kn resolver kn)
 
-let mind_of_delta mind = 
+let mind_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO idem *)
     Mod_subst.mind_of_delta resolver_param
-      (Mod_subst.mind_of_delta resolver mind)
-	
+      (Mod_subst.mind_of_delta_kn resolver kn)
+
+let exists_label id = exists_label id !global_env
+
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
     global_env := newenv;
-- 
cgit v1.2.3