3 files changed, 8 insertions, 6 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 2a84469af0..ec9a937f80 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1540,5 +1540,9 @@ let get g =
 
 end
 
+let is_construct_ref sigma c r =
+  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
+let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
+
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9662daa7c7..585db41de0 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -482,3 +482,6 @@ module MakeState(S : StateType) : sig
   val get : Proofview.Goal.t -> S.state
 
 end
+
+val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ccd0203b17..f55ece7d09 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -19,7 +19,6 @@ open Context
 open Vars
 open Locus
 open Printer
-open Globnames
 open Termops
 open Tacinterp
 
@@ -381,10 +380,6 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
-let is_construct_ref sigma c r =
-  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
-let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
-
 let rwcltac ?under cl rdx dir sr gl =
   let sr =
     let sigma, r = sr in
@@ -403,7 +398,7 @@ let rwcltac ?under cl rdx dir sr gl =
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
-      | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
+      | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ ->