diff options
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a2b5c8d70a..ebbec86b9c 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 @@ -511,7 +510,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +550,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with @@ -1163,6 +1162,9 @@ let error_bad_entry () = let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." +let error_inductive_bad_univs () = + str "Incorrect universe constrains declared for inductive type." + (* Recursion schemes errors *) let error_not_allowed_case_analysis env isrec kind i = @@ -1199,7 +1201,8 @@ let explain_inductive_error = function | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> - error_large_non_prop_inductive_not_in_type () + error_large_non_prop_inductive_not_in_type () + | BadUnivs -> error_inductive_bad_univs () (* Recursion schemes errors *) |