[cleanup] remove useless EConstr qualifications

2 files changed, 9 insertions, 9 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 9b52461def..f95672a15d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -906,11 +906,11 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
      mk_term ' ' (force_type ty) in
    let strip_cast (sigma, t) =
-    let open EConstr in
+     let open EConstr in
      let rec aux t = match kind_of_type sigma t with
-     | CastType (t, ty) when !n_binders = 0 && EConstr.isSort sigma ty -> t
-     | ProdType(n,s,t) -> decr n_binders; EConstr.mkProd (n, s, aux t)
-     | LetInType(n,v,ty,t) -> decr n_binders; EConstr.mkLetIn (n, v, ty, aux t)
+     | CastType (t, ty) when !n_binders = 0 && isSort sigma ty -> t
+     | ProdType(n,s,t) -> decr n_binders; mkProd (n, s, aux t)
+     | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
    let sigma, cty as ty = strip_cast (interp_term ist gl ty) in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index ada42a1c9b..7baccd3d75 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -36,15 +36,15 @@ module RelDecl = Context.Rel.Declaration
 let analyze_eliminator elimty env sigma =
   let open EConstr in
   let rec loop ctx t = match kind_of_type sigma t with
-  | AtomicType (hd, args) when EConstr.isRel sigma hd ->
-    ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
+  | AtomicType (hd, args) when isRel sigma hd ->
+    ctx, destRel sigma hd, not (Vars.noccurn sigma 1 t), Array.length args, t
   | CastType (t, _) -> loop ctx t
   | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
-  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (EConstr.Vars.subst1 b t)
+  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (Vars.subst1 b t)
   | _ ->
-    let env' = EConstr.push_rel_context ctx env in
+    let env' = push_rel_context ctx env in
     let t' = Reductionops.whd_all env' sigma t in
-    if not (EConstr.eq_constr sigma t t') then loop ctx t' else
+    if not (eq_constr sigma t t') then loop ctx t' else
       errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
       str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in