From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 toplevel/recordobj.ml | 77 ---------------------------------------------------
 1 file changed, 77 deletions(-)
 delete mode 100755 toplevel/recordobj.ml

(limited to 'toplevel/recordobj.ml')

diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
deleted file mode 100755
index d2a1e36e..00000000
--- a/toplevel/recordobj.ml
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: recordobj.ml,v 1.12.2.1 2004/07/16 19:31:49 herbelin Exp $ *)
-
-open Util
-open Pp
-open Names
-open Libnames
-open Nameops
-open Term
-open Instantiate
-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
-  add_anonymous_leaf (inObjDef1 sp);
-  List.iter
-    (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
-    comp
-
-let add_object_hook _ = objdef_declare
-- 
cgit v1.2.3