Merge pull request #25 from ppedrot/partial-fix

Fixing ML compilation with trunk.

1 files changed, 11 insertions, 15 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index b50635c..1c335f4 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
@@ -2889,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, (ty, _) =
+    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 = mkSsrConst "abstract_lock" env sigma in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in
-      let sigma = Sigma.to_evar_map sigma in
-      let sigma, abstract = mkSsrConst "abstract" env 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)