fix compilation on 8.5

1 files changed, 2 insertions, 4 deletions

diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index ea31101..7a2a473 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -4682,11 +4682,9 @@ let rec strip_unfold_term env ((sigma, t) as p) kt = match kind_of_term t with
       then strip_unfold_term env (sigma, f) kt
       else (sigma, f), true
   | Const (c,_) when Environ.is_projection c env ->
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma ((ty,_), sigma, _) =
+    let sigma, (ty, _) =
       Evarutil.new_type_evar env sigma (Evd.UnivFlexible true) in
-    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma ty in
-    let sigma = Sigma.to_evar_map sigma in
+    let sigma, ev = Evarutil.new_evar env sigma ty in
     (sigma, mkProj(Projection.make c false, ev)), true
   | Const _ | Var _ -> p, true
   | Proj _ -> p, true