diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 25a4804743..92b1ff7572 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -24,7 +24,7 @@ open Constrexpr_ops open Constrintern open Impargs open Reductionops -open Indtypes +open Type_errors open Pretyping open Indschemes open Context.Rel.Declaration @@ -304,7 +304,7 @@ let inductive_levels env evd poly arities inds = let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then - raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) + raise (InductiveError LargeNonPropInductiveNotInType) else evd else evd (* Evd.set_leq_sort env evd (Type cu) du *) |