diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 31706b3d01..24c0c47491 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -341,7 +341,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) - let ctx_body = restrict_universe_context ctx used_univs_body in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in |