diff options
| author | Emilio Jesus Gallego Arias | 2018-10-18 22:47:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-18 23:25:58 +0200 |
| commit | c3bafe593f431bf5ae1313a591a9ee719098a9f1 (patch) | |
| tree | dd79a69f29599a7360e318d7e3e91538465112e5 | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
[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.
| -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) |