diff options
| author | Matthieu Sozeau | 2014-03-12 12:21:40 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | ca318cd0d21ce157a3042b600ded99df6face25e (patch) | |
| tree | ca60f1337c739f46053aa904a1212c209052ef2e /proofs | |
| parent | df5e18302e113370906d9ca0b2a2e96dcaccbf0a (diff) | |
Fix issue #88: restrict_universe_context was wrongly forgetting about constraints,
and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f2da99c135..29810eb9ac 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -274,7 +274,7 @@ let close_proof ?feedback_id ~now fpl = let () = if poly || now then ignore (Future.compute univs) in let entries = Future.map2 (fun p (c, (t, octx)) -> let compute_univs (usubst, uctx) = - let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in + let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in let compute_c_t (c, eff) = let c, t = if not now then nf c, nf t @@ -283,9 +283,12 @@ let close_proof ?feedback_id ~now fpl = let univs = Univ.LSet.union (Universes.universes_of_constr c) (Universes.universes_of_constr t) - in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs in - (c, eff), t, Univ.ContextSet.to_context ctx + in + let ctx, subst = + Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) univs + in + let nf x = Vars.subst_univs_level_constr subst x in + (nf c, eff), nf t, Univ.ContextSet.to_context ctx in Future.chain ~pure:true p compute_c_t in |