diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -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 5bff3c813..8be96285f 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) -> |