diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 9 |
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; |