diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 21:01:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch) | |
| tree | bfd809fd50c8db88f390e3d5cba22360a0c90724 /proofs/proof_global.ml | |
| parent | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff) | |
Separate checking univ_decls and obtaining universe binder names.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fdc9a236b..9faff3211 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,8 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in - let binders = if poly then Some binders else None in + let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = |