Imported Upstream version 8.5~beta1+dfsg

1 files changed, 17 insertions, 37 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index ee1c94b9..5f2a2127 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -1,15 +1,12 @@
 (************************************************************************)
 (*  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 Util
-open Names
 open Libnames
-open Mod_subst
 
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
@@ -32,11 +29,11 @@ type 'a object_declaration = {
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
-  subst_function :  substitution * 'a -> 'a;
+  subst_function : Mod_subst.substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = anomaly s
+let yell s = Errors.anomaly (Pp.str s)
 
 let default_object s = {
   object_name = s;
@@ -69,12 +66,13 @@ type dynamic_object_declaration = {
   dyn_cache_function : object_name * obj -> unit;
   dyn_load_function : int -> object_name * obj -> unit;
   dyn_open_function : int -> object_name * obj -> unit;
-  dyn_subst_function : substitution * obj -> obj;
+  dyn_subst_function : Mod_subst.substitution * obj -> obj;
   dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
 
-let object_tag lobj = Dyn.tag lobj
+let object_tag = Dyn.tag
+let object_has_tag = Dyn.has_tag
 
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
@@ -82,36 +80,18 @@ let cache_tab =
 let declare_object_full odecl =
   let na = odecl.object_name in
   let (infun,outfun) = Dyn.create na in
-  let cacher (oname,lobj) =
-    if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the cachefun"
-  and loader i (oname,lobj) =
-    if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the loadfun"
-  and opener i (oname,lobj) =
-    if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the openfun"
-  and substituter (sub,lobj) = 
-    if Dyn.tag lobj = na then 
-      infun (odecl.subst_function (sub,outfun lobj))
-    else anomaly "somehow we got the wrong dynamic object in the substfun"
-  and classifier lobj =
-    if Dyn.tag lobj = na then
-      match odecl.classify_function (outfun lobj) with
-	| Dispose -> Dispose
-	| Substitute obj -> Substitute (infun obj)
-	| Keep obj -> Keep (infun obj)
-	| Anticipate (obj) -> Anticipate (infun obj)
-    else
-      anomaly "somehow we got the wrong dynamic object in the classifyfun"
+  let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
+  and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
+  and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
+  and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
+  and classifier lobj = match odecl.classify_function (outfun lobj) with
+  | Dispose -> Dispose
+  | Substitute obj -> Substitute (infun obj)
+  | Keep obj -> Keep (infun obj)
+  | Anticipate (obj) -> Anticipate (infun obj)
   and discharge (oname,lobj) =
-    if Dyn.tag lobj = na then
-      Option.map infun (odecl.discharge_function (oname,outfun lobj))
-    else
-      anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild lobj =
-    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
-    else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
+    Option.map infun (odecl.discharge_function (oname,outfun lobj))
+  and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
   in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;