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.ml | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 19da63b4d4..d879f4ee95 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -152,7 +152,7 @@ let abstract_constant_body c (hyps, subst) = let c = Vars.subst_vars subst c in it_mkLambda_or_LetIn c hyps -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = { |