diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-05 15:38:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-05 15:38:31 +0000 |
| commit | 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b (patch) | |
| tree | 26f5008ac4e4379128854cd3396c682c06792e94 /toplevel | |
| parent | 93db5abc5de50a6c43e2b94915cedce29b4a9c02 (diff) | |
Correction de bugs:
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
premier ordre : on revient sur l'algo tel qu'il était avant le
commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 5 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 488c39834..f34621216 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -105,8 +105,9 @@ let rec explain_exn_default_aux anomaly_string report_fn = function str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure:" ++ s ++ - if i=0 then mt () else str " (level " ++ int i ++ str").") + hov 0 (str "Error: Tactic failure" ++ + (if s <> mt() then str ":" ++ s else mt ()) ++ + if i=0 then str "." 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 ())) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 50d30cda7..a14d42074 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -485,7 +485,7 @@ let make_hunks etyps symbols from = let error_format () = error "The format does not match the notation." let rec split_format_at_ldots hd = function - | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt + | UnpTerminal s :: fmt when s = string_of_id ldots_var -> List.rev hd, fmt | u :: fmt -> check_no_ldots_in_box u; split_format_at_ldots (u::hd) fmt |