diff options
| author | Maxime Dénès | 2017-07-28 18:23:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-28 18:23:36 +0200 |
| commit | 3828267b6dcd60088a11fe0b9613871e4fc7c54f (patch) | |
| tree | acba2a7cbfb775ce570a13f1894a6f6161d3f617 /proofs | |
| parent | eaff3b36a178416f1828d75a4d46afc687953cea (diff) | |
| parent | 906b48ff401f22be6059a6cdde8723b858102690 (diff) | |
Merge PR #888: Stronger kernel types
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 6 |
2 files changed, 7 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a949c8e911..1937885587 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body - (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in - let (cb, ctx), se = Future.force ce.const_entry_body in + (fun (pt, _) -> pt, ()) } in + let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 52d6787d44..2ade797f63 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let univs = + if poly then Entries.Polymorphic_const_entry univs + else Entries.Monomorphic_const_entry univs + in { Entries. const_entry_body = body; const_entry_secctx = section_vars; @@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_inline_code = false; const_entry_opaque = true; const_entry_universes = univs; - const_entry_polymorphic = poly}) + }) fpl initial_goals in let binders = Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) |