From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 pretyping/recordops.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3d97d8b2..78626854 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,14 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*)
 
 (*i*)
 open Names
 open Nametab
 open Term
 open Libnames
-open Classops
 open Libobject
 open Library
 (*i*)
-- 
cgit v1.2.3