diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/API/API.mli b/API/API.mli index ecce22c1de..899bafa1fd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1088,12 +1088,11 @@ sig | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration - type abstrac_inductive_universes = Declarations.abstrac_inductive_universes = + type abstract_inductive_universes = Declarations.abstract_inductive_universes = | Monomorphic_ind of Univ.UContext.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info - type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1103,7 +1102,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_universes : abstrac_inductive_universes; + mind_universes : Declarations.abstract_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } |