diff options
| author | herbelin | 2006-02-07 22:11:50 +0000 |
|---|---|---|
| committer | herbelin | 2006-02-07 22:11:50 +0000 |
| commit | 634e6ddaecc6f6bf577c39d6b146e7d75fb79c74 (patch) | |
| tree | e72b848a7fa7f74efd00aec93062cf38a0365fc7 /toplevel | |
| parent | b4d90fd1babe9a78dae9431aa466a197625bf3d6 (diff) | |
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
prédicat de filtrage après le terme filtré conformément à l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |