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