From bf0499bc507d5a39c3d5e3bf1f69191339270729 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Oct 2015 18:18:01 +0200
Subject: Fix LemmaOverloading

Do not normalize the type of a proof according to the final universes
when keep_body_ucst_separate is true, otherwise the type might not be
retypable in the initial context...
---
 proofs/proof_global.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3e06294e64..a0ead42ef3 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -313,7 +313,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
     if poly || now then
       let make_body t (c, eff) =
         let open Universes in
-        let body = c and typ = nf t in
+        let body = c in
+	let typ =
+	  if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then
+	    nf t
+	  else t
+	in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
         if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then
-- 
cgit v1.2.3