From 9961577dfbb93f0b691c355ba99822665def037f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 17:00:48 +0200 Subject: Using a record type for Cooking.result. --- kernel/cooking.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 95822fac6..63614e20f 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -151,9 +151,14 @@ let abstract_constant_body = type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - constant_universes * inline * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : constant_type; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} let on_body ml hy f = function | Undef _ as x -> x @@ -254,9 +259,14 @@ let cook_constant ~hcons env { from = cb; info } = | Polymorphic_const auctx -> Polymorphic_const (AUContext.union abs_ctx auctx) in - (body, typ, Option.map projection cb.const_proj, - univs, cb.const_inline_code, - Some const_hyps) + { + cook_body = body; + cook_type = typ; + cook_proj = Option.map projection cb.const_proj; + cook_universes = univs; + cook_inline = cb.const_inline_code; + cook_context = Some const_hyps; + } (* let cook_constant_key = Profile.declare_profile "cook_constant" *) (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) -- cgit v1.2.3