diff options
| -rw-r--r-- | vernac/comInductive.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 3e1e9ceaf1..067fb3d2ca 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -67,7 +67,3 @@ val template_polymorphism_candidate : can be made parametric in its conclusion sort, if one is given. If the [Template Check] flag is false we just check that the conclusion sort is not small. *) - -val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t -(** [sign_level env sigma ctx] computes the universe level of the context [ctx] - as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) |