diff options
| author | Gaëtan Gilbert | 2019-01-10 14:43:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 5f9a6c17b4353024e7510977a41cfb1de93a0f5f (patch) | |
| tree | 90cad909e39d662f6d7f7293d47c242edd9d4d8e /vernac | |
| parent | 05e2222e04323d11429d659b415750cf40e2babd (diff) | |
Move inductive_error to Type_errors
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 4 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 1 | ||||
| -rw-r--r-- | vernac/himsg.ml | 1 | ||||
| -rw-r--r-- | vernac/himsg.mli | 1 |
4 files changed, 2 insertions, 5 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 *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index e1496e58d7..71770a21ca 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -10,7 +10,6 @@ open Pp open CErrors -open Indtypes open Type_errors open Pretype_errors open Indrec diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f3e1e1fc49..98c8c21699 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -15,7 +15,6 @@ open Nameops open Namegen open Constr open Termops -open Indtypes open Environ open Pretype_errors open Type_errors diff --git a/vernac/himsg.mli b/vernac/himsg.mli index bab66b2af4..986906d303 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Indtypes open Environ open Type_errors open Pretype_errors |