1 files changed, 0 insertions, 65 deletions
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index 6457fb538..4c1e2210a 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -8,68 +8,3 @@
 
 (* $Id$ *)
 
-open Util
-open Pp
-open Names
-open Libnames
-open Nameops
-open Term
-open Lib
-open Declare
-open Recordops
-open Classops
-open Nametab
-
-(*****  object definition ******)
- 
-let typ_lams_of t = 
-  let rec aux acc c = match kind_of_term c with
-    | Lambda (x,c1,c2) -> aux (c1::acc) c2
-    | Cast (c,_) -> aux acc c
-    | t -> acc,t
-  in aux [] t
-
-let objdef_err ref =
-  errorlabstrm "object_declare"
-    (pr_id (id_of_global ref) ++
-       str" is not a structure object")
-
-let objdef_declare ref =
-  let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
-  let env = Global.env () in
-  let v = constr_of_reference ref in
-  let vc = match Environ.constant_opt_value env sp with
-    | Some vc -> vc
-    | None -> objdef_err ref in
-  let lt,t = decompose_lam vc in
-  let lt = List.rev (List.map snd lt) in
-  let f,args = match kind_of_term t with
-    | App (f,args) -> f,args 
-    | _ -> objdef_err ref in
-  let { s_PARAM = p; s_PROJ = lpj } = 
-    try (find_structure
-	   (match kind_of_term f with
-              | Construct (indsp,1) -> indsp
-	      | _ -> objdef_err ref))
-    with Not_found -> objdef_err ref in
-  let params, projs =
-    try list_chop p (Array.to_list args)
-    with _ -> objdef_err ref in
-  let lps = 
-    try List.combine lpj projs 
-    with _ -> objdef_err ref in
-  let comp =
-    List.fold_left
-      (fun l (spopt,t) -> (* comp=components *)
-	 match spopt with
-	   | None -> l
-           | Some proji_sp ->
-	       let c, args = decompose_app t in
-	       try (ConstRef proji_sp, reference_of_constr c, args) :: l
-               with Not_found -> l)
-      [] lps in
-  let comp' = List.map (fun (refi,c,argj) ->
-    (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in
-  add_canonical_structure (sp, comp')
-
-let add_object_hook _ = objdef_declare