diff options
| author | Matthieu Sozeau | 2015-05-27 11:43:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-05-27 11:43:11 +0200 |
| commit | 866c41b9720413e00194ba7addb9c4277e114890 (patch) | |
| tree | 37fe660b28acfbaa6f3f304b6b9f3eebcf15dddb /proofs | |
| parent | ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (diff) | |
Fix bug #4159
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5bff3c8131..8be96285f9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -292,7 +292,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let body = c and typ = nf t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - let ctx = Evd.evar_universe_context_set universes in + let ctx = Evd.evar_universe_context_set Univ.UContext.empty universes in if keep_body_ucst_sepatate then (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of @@ -317,7 +317,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context universes in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt, Evd.evar_universe_context_set (Future.force univs)), eff) + (pt, Evd.evar_universe_context_set initunivs (Future.force univs)), eff) in let entries = Future.map2 (fun p (_, t) -> |