From 1a2dc1bb8b78b07ea7620b466138f43df6a05aaa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Nov 1999 21:16:04 +0000
Subject: Maintenant compilable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@155 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9f858ed1df..cc2719ba31 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -5,14 +5,15 @@ open Util
 open Pp
 open Names
 open Typeops
-open Vartab
 open Libobject
 open Library
+(*
 open Term
 open Pp_control
 open Generic
 open Initial
 open Classops
+*)
 
 let nbimpl = ref 0
 let nbpathc = ref 0
@@ -39,6 +40,7 @@ let (inStruc,outStruc) =
     declare_object ("STRUCTURE",
                     {load_function = (fun _ -> ());
                      cache_function = (function  (_,x) -> add_new_struc1 x);
+		     open_function = (fun _ -> ());
                      specification_function = (function x -> x)})
 
 let add_new_struc (s,c,n,l) = 
-- 
cgit v1.2.3