diff options
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 327e697d2..eb4073096 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,7 +19,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option val cook_constant : env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr |