diff options
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/recordops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 0af25666d4..74a0d7d8ec 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -13,7 +13,6 @@ open Names open Nametab open Term open Libnames -open Classops open Libobject open Library (*i*) |