From 8966c9241207b6f5d4ee38508246ee97ed006e72 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 31 Jul 2017 16:49:06 +0200 Subject: proof_global: cleanup and comment close_proof evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. --- vernac/lemmas.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'vernac/lemmas.ml') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d78cd14f6..793022377 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -510,8 +510,10 @@ let save_proof ?proof = function let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.check_univ_decl evd decl in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), - (universes, Some binders)) + let poly = pi2 k in + let binders = if poly then Some binders else None in + Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> -- cgit v1.2.3