diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 7 | ||||
| -rw-r--r-- | toplevel/himsg.mli | 3 |
3 files changed, 12 insertions, 0 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 8342d6800b..35725c5bf1 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -79,6 +79,8 @@ let rec explain_exn_default = function | Cases.PatternMatchingError (env,e) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) + | Tacred.ReductionTacticError e -> + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c870e71826..844accb3af 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -33,6 +33,7 @@ let quote s = h 0 (str "\"" ++ s ++ str "\"") let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) +let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let nth i = @@ -682,3 +683,9 @@ let explain_pattern_matching_error env = function explain_non_exhaustive env tms | CannotInferPredicate typs -> explain_cannot_infer_predicate env typs + +let explain_reduction_tactic_error = function + | Tacred.InvalidAbstraction (env,c,(env',e)) -> + str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++ + spc() ++ str "is not well typed." ++ fnl () ++ + explain_type_error env' e diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index cacdf9b0c2..05a52b8b75 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -34,3 +34,6 @@ val explain_refiner_error : refiner_error -> std_ppcmds val explain_pattern_matching_error : env -> pattern_matching_error -> std_ppcmds + +val explain_reduction_tactic_error : + Tacred.reduction_tactic_error -> std_ppcmds |