3 files changed, 6 insertions, 7 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a284c3bfc7..5d75b28539 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -940,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m =
 
 let pf_partial_solution gl t evl =
   let sigma, g = project gl, sig_it gl in
-  let sigma = Goal.V82.partial_solution sigma g t in
+  let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in
   re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma
 
 let dependent_apply_error =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index c04ced4ab4..036b20bfcd 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -433,15 +433,15 @@ let lz_coq_prod =
 
 let lz_setoid_relation =
   let sdir = ["Classes"; "RelationClasses"] in
-  let last_srel = ref (Environ.empty_env, None) in
+  let last_srel = ref None in
   fun env -> match !last_srel with
-  | env', srel when env' == env -> srel
+  | Some (env', srel) when env' == env -> srel
   | _ ->
     let srel =
        try Some (UnivGen.constr_of_global @@
                  Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
        with _ -> None in
-    last_srel := (env, srel); srel
+    last_srel := Some (env, srel); srel
 
 let ssr_is_setoid env =
   match lz_setoid_relation env with
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 940defb743..4ed75cdbe4 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -170,10 +170,9 @@ let declare_one_prenex_implicit locality f =
 }
 
 VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
-  | [ "Prenex" "Implicits" ne_global_list(fl) ]
+  | #[ locality = Attributes.locality; ] [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
-         let open Vernacinterp in
-         let locality = Locality.make_section_locality atts.locality in
+         let locality = Locality.make_section_locality locality in
          List.iter (declare_one_prenex_implicit locality) fl;
      }
 END