diff options
Diffstat (limited to 'kernel/indTyping.mli')
| -rw-r--r-- | kernel/indTyping.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 723ba5459e..babb82c39e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option -> mutual_inductive_entry -> env * universes + * template_universes option * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context @@ -44,4 +45,4 @@ val template_polymorphic_univs : Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> - Univ.Level.t option list * Univ.LSet.t + (Univ.LSet.t * Univ.Level.t option list) option |