diff options
author | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /pretyping/recordops.mli | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Imported Upstream version 8.0pl3upstream/8.0pl3
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; |