diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7b9ad313..ff090ca8 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -10,12 +10,10 @@ open Loc open Names open Constrexpr open Libnames -open Globnames open Nametab open Genredexpr open Genarg open Pattern -open Decl_kinds open Misctypes open Locus |