aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-07-31 16:49:06 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2017-09-19 10:28:03 +0200
commit8966c9241207b6f5d4ee38508246ee97ed006e72 (patch)
tree774d61f09e653e084c9fc1c1b5fd01996ab09a76 /vernac
parentd9e54d65cc808eab2908beb7a7a2c96005118ace (diff)
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.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/lemmas.ml6
1 files changed, 4 insertions, 2 deletions
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) ->