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.mli | |
| parent | 4457e6d75affd20c1c13c0d798c490129525bcb5 (diff) | |
Using a record type for Cooking.result.
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 79a028d76..f386fd936 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,9 +16,14 @@ 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; +} val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr |