From 29f6948c82da7ef51562a49d069583ffe77aa0ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 19 Dec 2016 13:09:34 +0100
Subject: fix compilation on 8.5

---
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 6 ++----
 1 file 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
-- 
cgit v1.2.3