diff options
| author | Gaëtan Gilbert | 2018-10-20 22:16:22 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-20 22:16:22 +0200 |
| commit | fd214f1ad31d88c76dd928b6c6b039eaefcb21db (patch) | |
| tree | 10327a156140bb6e671237ebac7cb6459247346e | |
| parent | 16e0223e111cdf1c61c421617dfda08de6e96720 (diff) | |
| parent | c3bafe593f431bf5ae1313a591a9ee719098a9f1 (diff) | |
Merge PR #8769: [library] Remove redundant re-addition of universe constraints.
| -rw-r--r-- | interp/declare.ml | 9 |
1 files changed, 1 insertions, 8 deletions
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) |