diff options
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index f042de00f..c85d51667 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -8,11 +8,7 @@ open Loc open Names -open Libnames -open Misctypes -open Decl_kinds open Constrexpr -open Notation_term (** Topconstr *) |