diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 17db25660f..4d7a04f5ee 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -36,7 +36,6 @@ open Ppconstr open Printer open Globnames open Namegen -open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops |