diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-12-11 17:59:42 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-12-11 18:00:25 +0100 |
| commit | 3c81c6c3b595ef06e0c01e51775aa0118f44e421 (patch) | |
| tree | 615c6e8749a3f99776fb3927a7778f25f4af6102 /proofs/proof_global.ml | |
| parent | 119d61453c6761f20b8862f47334bfb8fae0049e (diff) | |
Univs: Fix bug #4363, nested abstract.
Diffstat (limited to 'proofs/proof_global.ml')
| -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 3d60ff217..3edd34e5f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -333,7 +333,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 |