aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrcommon.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-rw-r--r--plugins/ssr/ssrcommon.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ea7216832..2a31157be 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
open Globnames
-open Misctypes
open Decl_kinds
let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)