From c3bafe593f431bf5ae1313a591a9ee719098a9f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Oct 2018 22:47:58 +0200
Subject: [library] Remove redundant re-addition of universe constraints.

After some analysis this should be taken care of by
`Safe_typing.add_constant`

It was added in
https://github.com/coq/coq/commit/f7338257584ba69e7e815c7ef9ac0d24f0dec36c
, so maybe @gares can provide more context as to how is this stuff
supposed to work.
---
 interp/declare.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 07a0066ea8..7a32018c0e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) =
   if obj.cst_locl then ()
   else
     let con = Global.constant_of_delta_kn kn in
-    Nametab.push (Nametab.Exactly i) sp (ConstRef con);
-    match (Global.lookup_constant con).const_body with
-    | (Def _ | Undef _) -> ()
-    | OpaqueDef lc ->
-        match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
-        | Some f when Future.is_val f ->
-	   Global.push_context_set false (Future.force f)
-        | _ -> ()
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
   variable_exists id || Global.exists_objlabel (Label.of_id id)
-- 
cgit v1.2.3