From 3c81c6c3b595ef06e0c01e51775aa0118f44e421 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Dec 2015 17:59:42 +0100 Subject: Univs: Fix bug #4363, nested abstract. --- proofs/proof_global.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'proofs') 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 -- cgit v1.2.3