diff options
| author | Pierre-Marie Pédrot | 2019-05-15 23:50:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:14:19 +0200 |
| commit | 801aed67a90ec49c15a4469e1905aa2835fabe19 (patch) | |
| tree | 9da139e5e0e5ecd8ba74806d2baa1225cee2e720 /kernel/cooking.mli | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index d218dd36da..ffd4e51ffc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -13,7 +13,7 @@ open Declarations (** {6 Cooking the constants. } *) -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool |