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(-)

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