diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 5429e660..8f380830 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -783,7 +783,7 @@ let explain_pretype_error env sigma err = let {uj_val = c; uj_type = actty} = j in let (env, c, actty, expty), e = contract3' env c actty t e in let j = {uj_val = c; uj_type = actty} in - explain_actual_type env sigma j t (Some e) + explain_actual_type env sigma j expty (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp | VarNotFound id -> explain_var_not_found env id @@ -872,11 +872,11 @@ let explain_not_match_error = function quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = - str "Signature components for label " ++ str (Label.to_string l) ++ + str "Signature components for label " ++ pr_label l ++ str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." let explain_label_already_declared l = - str ("The label "^Label.to_string l^" is already declared.") + str "The label " ++ pr_label l ++ str " is already declared." let explain_application_to_not_path _ = strbrk "A module cannot be applied to another module application or " ++ @@ -924,9 +924,6 @@ let explain_label_missing l s = str "The field " ++ str (Label.to_string l) ++ str " is missing in " ++ str s ++ str "." -let explain_higher_order_include () = - str "You cannot Include a higher-order structure." - let explain_module_error = function | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l @@ -943,7 +940,6 @@ let explain_module_error = function | IncorrectWithConstraint l -> explain_incorrect_label_constraint l | GenerativeModuleExpected l -> explain_generative_module_expected l | LabelMissing (l,s) -> explain_label_missing l s - | HigherOrderInclude -> explain_higher_order_include () (* Module internalization errors *) @@ -1086,7 +1082,7 @@ let error_bad_ind_parameters env c n v1 v2 = let pv1 = pr_lconstr_env env Evd.empty v1 in let pv2 = pr_lconstr_env env Evd.empty v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ - str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." + str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = str "The name" ++ spc () ++ pr_id id ++ spc () ++ @@ -1170,18 +1166,18 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if Int.equal n 0 then "no "^s^"s" - else if Int.equal n 1 then "1 "^s - else (string_of_int n^" "^s^"s") + if Int.equal n 0 then str "no " ++ str s ++ str "s" + else if Int.equal n 1 then str "1 " ++ str s + else (int n ++ str " " ++ str s ++ str "s") let explain_wrong_numarg_constructor env cstr n = str "The constructor " ++ pr_constructor env cstr ++ str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++ - str ") expects " ++ str (decline_string n "argument") ++ str "." + str ") expects " ++ decline_string n "argument" ++ str "." let explain_wrong_numarg_inductive env ind n = str "The inductive type " ++ pr_inductive env ind ++ - str " expects " ++ str (decline_string n "argument") ++ str "." + str " expects " ++ decline_string n "argument" ++ str "." let explain_unused_clause env pats = (* Without localisation |