diff options
| author | Maxime Dénès | 2017-07-28 18:23:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-28 18:23:36 +0200 |
| commit | 3828267b6dcd60088a11fe0b9613871e4fc7c54f (patch) | |
| tree | acba2a7cbfb775ce570a13f1894a6f6161d3f617 /kernel/cooking.mli | |
| parent | eaff3b36a178416f1828d75a4d46afc687953cea (diff) | |
| parent | 906b48ff401f22be6059a6cdde8723b858102690 (diff) | |
Merge PR #888: Stronger kernel types
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 79a028d760..f386fd9362 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 |