From 57cc7ecae9378ceaa863ae8fd32bc767100c54e0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 Feb 2016 13:20:42 +0100
Subject: Fixing ML compilation with trunk.

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index b50635c..ea79452 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -109,10 +109,12 @@ let mkSsrRef name =
   Errors.error "Small scale reflection library not loaded"
 let mkSsrRRef name = GRef (dummy_loc, mkSsrRef name,None), None
 let mkSsrConst name env sigma =
-  Evd.fresh_global env sigma (mkSsrRef name)
+  Sigma.fresh_global env sigma (mkSsrRef name)
 let pf_mkSsrConst name gl =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
-  let sigma, t = mkSsrConst name env sigma in
+  let sigma = Sigma.Unsafe.of_evar_map sigma in
+  let Sigma (t, sigma, _) = mkSsrConst name env sigma in
+  let sigma = Sigma.to_evar_map sigma in
   t, re_sig it sigma
 let pf_fresh_global name gl =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
@@ -2891,13 +2893,13 @@ let ssrmkabs id gl =
   let step = { run = begin fun sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let sigma, abstract_proof, abstract_ty =
-      let sigma, (ty, _) =
-        Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
-      let sigma, ablock = mkSsrConst "abstract_lock" env sigma in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma ((ty, _), sigma, _) =
+        Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
+      let Sigma (ablock, sigma, _) = mkSsrConst "abstract_lock" env sigma in
       let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in
+      let Sigma (abstract, sigma, _) = mkSsrConst "abstract" env sigma in
       let sigma = Sigma.to_evar_map sigma in
-      let sigma, abstract = mkSsrConst "abstract" env sigma in
       let abstract_ty = mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (m, sigma, _) = Evarutil.new_evar env sigma abstract_ty in
-- 
cgit v1.2.3


From 442df41ec75a51598be771f981ae17dd8d385481 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 Feb 2016 13:26:23 +0100
Subject: Removing compatibility layers.

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index ea79452..1c335f4 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -2891,23 +2891,17 @@ let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id
 let ssrmkabs id gl =
   let env, concl = pf_env gl, pf_concl gl in
   let step = { run = begin fun sigma ->
-    let sigma = Sigma.to_evar_map sigma in
-    let sigma, abstract_proof, abstract_ty =
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma ((ty, _), sigma, _) =
+    let Sigma ((abstract_proof, abstract_ty), sigma, p) =
+      let Sigma ((ty, _), sigma, p1) =
         Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
-      let Sigma (ablock, sigma, _) = mkSsrConst "abstract_lock" env sigma in
-      let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in
-      let Sigma (abstract, sigma, _) = mkSsrConst "abstract" env sigma in
-      let sigma = Sigma.to_evar_map sigma in
+      let Sigma (ablock, sigma, p2) = mkSsrConst "abstract_lock" env sigma in
+      let Sigma (lock, sigma, p3) = Evarutil.new_evar env sigma ablock in
+      let Sigma (abstract, sigma, p4) = mkSsrConst "abstract" env sigma in
       let abstract_ty = mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (m, sigma, _) = Evarutil.new_evar env sigma abstract_ty in
-      let sigma = Sigma.to_evar_map sigma in
-      sigma, m, abstract_ty in
+      let Sigma (m, sigma, p5) = Evarutil.new_evar env sigma abstract_ty in
+      Sigma ((m, abstract_ty), sigma, p1 +> p2 +> p3 +> p4 +> p5) in
     let sigma, kont =
       let rd = Name id, None, abstract_ty in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (ev, sigma, _) = Evarutil.new_evar (Environ.push_rel rd env) sigma concl in
       let sigma = Sigma.to_evar_map sigma in
       (sigma, ev)
-- 
cgit v1.2.3