From 7d697193ab175b6bfa3c773880c0a06348449d19 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 18 Oct 2015 20:29:58 +0200
Subject: Making Evarutil.new_evar monotonous.

---
 proofs/proofview.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f549913f2f..bc2cc3e913 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -65,7 +65,9 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+    let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
-- 
cgit v1.2.3