diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f3b7ae2b24..21651b3e21 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -169,7 +169,7 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } -type abstrac_inductive_universes = +type abstract_inductive_universes = | Monomorphic_ind of Univ.universe_context | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info @@ -192,7 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) |