From 2de8910d2cc0af096e6d91b0ea165997ce144503 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 May 2014 11:34:53 +0200
Subject: - Fix treatment of global universe constraints which should be passed
 along in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value
 of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. -
 Fix a HUGE performance problem in the processing of constraints, which was
 remerging all the previous constraints with the ambient global universes at
 each new constraint addition. Performance is now back to (or better than)
 normal.

---
 proofs/proof_global.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e49a57af39..5cb677d1c6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -226,7 +226,7 @@ let start_proof id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.start Evd.empty goals;
+    proof = Proof.start (Evd.from_env (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
@@ -237,7 +237,7 @@ let start_dependent_proof id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.dependent_start Evd.empty goals;
+    proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
-- 
cgit v1.2.3