2 files changed, 6 insertions, 5 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 8cb0a8b463..efd65ade15 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -122,6 +122,7 @@ let add_genarg tag pr =
 
 (** Constructors for cast type *)
 let dC t = CastConv t
+
 (** Constructors for constr_expr *)
 let isCVar   = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false
 let destCVar = function
@@ -139,6 +140,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((CAst.make ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
+
 (** Constructors for rawconstr *)
 let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
@@ -896,7 +898,7 @@ let interp_rpattern s = function
 
 let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
 
-type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option
+type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
 let tag_of_cpattern = pi1
 let loc_of_cpattern = loc_ofCG
 let cpattern_of_term (c, t) ist = c, t, Some ist
@@ -925,7 +927,7 @@ let of_ftactic ftac gl =
   let tac = Proofview.V82.of_tactic tac in
   let { sigma = sigma } = tac gl in
   let ans = match !r with
-  | None -> assert false (** If the tactic failed we should not reach this point *)
+  | None -> assert false (* If the tactic failed we should not reach this point *)
   | Some ans -> ans
   in
   (sigma, ans)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 93a8c48435..f0bb6f58a6 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -5,9 +5,7 @@ open Goal
 open Environ
 open Evd
 open Constr
-
-open Ltac_plugin
-open Tacexpr
+open Genintern
 
 (** ******** Small Scale Reflection pattern matching facilities ************* *)
 
@@ -196,6 +194,7 @@ val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> c
 
 (** [do_once r f] calls [f] and updates the ref only once *)
 val do_once : 'a option ref -> (unit -> 'a) -> unit
+
 (** [assert_done r] return the content of r. @raise Anomaly is r is [None] *)
 val assert_done : 'a option ref -> 'a