From 249a1910a2474216b7f98491afafc6019a04c894 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Wed, 24 May 2017 23:46:23 +0200
Subject: Remove Warnings: unused value ...

---
 proofs/proof_global.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f5664aed0..d5fbdbb83 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -336,7 +336,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let make_body =
     if poly || now then
       let make_body t (c, eff) =
-        let open Universes in
         let body = c in
 	let typ =
 	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
-- 
cgit v1.2.3