diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /kernel/cooking.mli | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7d47eba23..9db85a4a1 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,8 +18,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr |