From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 13:38:22 +0200 Subject: More precise type for universe entries. We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. --- proofs/proof_global.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 52d6787d4..2ade797f6 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))) -- cgit v1.2.3