diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 96392edb11..217381d854 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -27,7 +27,6 @@ open Glob_ops open Pattern open Notation open Detyping -open Decl_kinds module NamedDecl = Context.Named.Declaration (*i*) |