diff options
Diffstat (limited to 'toplevel/recordobj.ml')
| -rwxr-xr-x | toplevel/recordobj.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 654c1bd3f..918909c79 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -14,7 +14,6 @@ open Names open Libnames open Nameops open Term -open Instantiate open Lib open Declare open Recordops |