diff options
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4363.v | 7 |
2 files changed, 9 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3d60ff217a..3edd34e5f6 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 diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v new file mode 100644 index 0000000000..75a9c9a041 --- /dev/null +++ b/test-suite/bugs/closed/4363.v @@ -0,0 +1,7 @@ +Set Printing Universes. +Definition foo : Type. +Proof. + assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat). + exact bar. +Defined. (* Toplevel input, characters 0-8: +Error:
\ No newline at end of file |