From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- proofs/proof_global.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index ea0408169..905173efc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,7 +331,7 @@ 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 univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let univctx = UState.check_univ_decl 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 @@ -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 = UState.check_univ_decl 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 = UState.check_univ_decl 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 = UState.check_univ_decl bodyunivs universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = @@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let univs, typ = Future.force univstyp in let univs = if poly then Entries.Polymorphic_const_entry univs - else Entries.Monomorphic_const_entry univs + else + (* FIXME be smarter about the unnecessary context linearisation in make_body *) + Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs) in {Entries. const_entry_body = body; -- cgit v1.2.3