Imported Upstream version 8.0pl3upstream/8.0pl3

1 files changed, 1 insertions, 8 deletions

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 66c1f34d..a458b7b3 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli,v 1.15.2.1 2004/07/16 19:30:46 herbelin Exp $ i*)
+(*i $Id: recordops.mli,v 1.15.2.2 2005/11/29 21:40:52 letouzey Exp $ i*)
 
 (*i*)
 open Names
@@ -18,13 +18,6 @@ open Libobject
 open Library
 (*i*)
 
-val nbimpl : int ref
-val nbpathc : int ref
-val nbcoer : int ref
-val nbstruc : int ref
-val nbimplstruc : int ref
-val compter : bool ref
-
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;