Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 12 insertions, 8 deletions

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;