diff options
| author | Emilio Jesus Gallego Arias | 2019-10-24 21:08:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-25 00:12:03 +0200 |
| commit | bd27f8b3c9894a73f3f93662f6ff11dfb8fb65c4 (patch) | |
| tree | 42baf0a82c2ebf1aee8fae0c52b8ebaf68b57ed7 | |
| parent | 1923e2a87e8754e63e8d9edcdfe178a841ff96d2 (diff) | |
[vernac] [inductive] Remove unused internal export.
| -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] *) |