diff options
| author | herbelin | 2003-03-31 21:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-31 21:18:53 +0000 |
| commit | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (patch) | |
| tree | 0bd65009594d83c85a6e3f4f5bf8a0e77e0b4fc6 /toplevel | |
| parent | ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 (diff) | |
Ajout d'un message à FailTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 45fe9995ef..d0be357d5d 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -84,8 +84,10 @@ let rec explain_exn_default = function | Nametab.GlobalizationConstantError q -> hov 0 (str "Error:" ++ spc () ++ str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q) - | Refiner.FailError i -> - hov 0 (str "Error: Tactic failed (level " ++ int i ++ str").") + | Refiner.FailError (i,s) -> + let s = if s="" then "" else " \""^s^"\"" in + hov 0 (str "Error: Tactic failure" ++ str s ++ + if i=0 then mt () else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) |