diff options
| author | Gaëtan Gilbert | 2017-12-05 20:22:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-06 13:23:31 +0100 |
| commit | 5b8b02cd060097c3c980b0498257c30eda1ad207 (patch) | |
| tree | ff0e51230d3518bb2db523187644cd73d40aecf5 /proofs | |
| parent | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (diff) | |
Fix #6323: stronger restrict universe context vs abstract.
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 12 |
2 files changed, 5 insertions, 8 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 31a73db04f..6b503a0112 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); + let univs = UState.demote_seff_univs const univs in const, status, univs with reraise -> let reraise = CErrors.push reraise in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 535ef2013d..167d6bda0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,13 +348,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in - (* Universes for private constants are relevant to the body *) - let used_univs_body = - List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) - used_univs_body (Safe_typing.universes_of_private eff) - in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in @@ -362,7 +358,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now (* 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) |