diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 17:00:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:14 +0200 |
| commit | 9961577dfbb93f0b691c355ba99822665def037f (patch) | |
| tree | 11f7fc112285f2f64118441937f47cf4d1236c29 /kernel/cooking.ml | |
| parent | 4457e6d75affd20c1c13c0d798c490129525bcb5 (diff) | |
Using a record type for Cooking.result.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 22 |
1 files changed, 16 insertions, 6 deletions
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 *) |