From 91b1808056602f3e26d1eb1bdf7be1e791cb742d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:35:07 +0200
Subject: Univs: fix many evar_map initializations and leaks.

---
 stm/lemmas.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 7679b1a662..2bd1c54519 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -503,4 +503,5 @@ let save_proof ?proof = function
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+    let env = Global.env () in
+    (Evd.from_env env, env)
-- 
cgit v1.2.3


From 11cdf7c2ca0017f6bae906f9c9d9eef41972affe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 15:16:06 +0200
Subject: Univs: fix handling of side effects/delayed proofs

- When there are side effects which might enrich the initial universes
  of a proof, keep the initial and refined universe contexts apart like
  for delayed proofs, ensuring universes are declared before they are
  used in the right order.
- Fix undefined levels in proof statements so that they can't be lowered
  to Set by a subsequent, delayed proof.
---
 stm/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 2bd1c54519..16444fda05 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,7 +449,7 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  start_proof_with_initialization kind evd
+  start_proof_with_initialization kind (Evd.fix_undefined_variables evd)
     recguard thms snl hook
 
 
-- 
cgit v1.2.3


From b8a85b65432a974d6a6f1fe5165e05d7196c9321 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:33:27 +0200
Subject: Univs: fix semantics of Type in proof mode in universe-polymorphic
 mode

Allowing universes to be instantiated if the body of the proof
requires it (the levels stay flexible). Not allowed for non-polymorphic
cases, to be compatible with the stm's invariant that the type should
not change.
---
 stm/lemmas.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 16444fda05..5cbe152b55 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,8 +449,12 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  start_proof_with_initialization kind (Evd.fix_undefined_variables evd)
-    recguard thms snl hook
+  let evd =
+    if pi2 kind then evd
+    else (* We fix the variables to ensure they won't be lowered to Set *)
+      Evd.fix_undefined_variables evd
+  in
+    start_proof_with_initialization kind evd recguard thms snl hook
 
 
 (* Saving a proof *)
-- 
cgit v1.2.3