diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 10:30:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 10:38:52 +0100 |
| commit | db282f831cbf619e417593c602de24960c3ca69c (patch) | |
| tree | 6f4bcc1830e37713c571e58084214571c8920ff1 /proofs | |
| parent | f439001caa24671d03d8816964ceb8e483660e70 (diff) | |
| parent | ce395ca02311bbe6ecc1b2782e74312272dd15ec (diff) | |
Merge branch 'v8.5'
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 31706b3d0..24c0c4749 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 |