diff options
| author | herbelin | 2000-11-08 15:59:09 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-08 15:59:09 +0000 |
| commit | 0b1c4218edbe9c1e43b0b62941905ed2c7d7a848 (patch) | |
| tree | a7b9b94948de81cb6ec1681637542753ca9b03f9 | |
| parent | 5af1af3bce9ddad4056967fb48f1d7fca6615b1a (diff) | |
amélioration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@827 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/himsg.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 2a88052326..a4a089bd5f 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -107,9 +107,9 @@ let explain_actual_type k ctx c ct pt = let pct = prterm_env ctx ct in let pt = prterm_env ctx pt in [< pe; 'fNL; - 'sTR"The term"; 'bRK(1,1); pc ; 'sPC ; - 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL; - 'sTR"Actually, it has type" ; 'bRK(1,1); pct >] + 'sTR "The term"; 'bRK(1,1); pc ; 'sPC ; + 'sTR "has type" ; 'bRK(1,1); pct; 'bRK(1,1); + 'sTR "while it is expected to have type"; 'bRK(1,1); pt >] let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl = let ctx = make_all_name_different ctx in @@ -147,7 +147,7 @@ let explain_cant_apply_not_functional k ctx rator randl = hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in [< 'sTR"Illegal application (Non-functional construction): "; (* pe; *) 'fNL; - 'sTR"The term"; 'bRK(1,1); pr; 'sPC; + 'sTR"The expression"; 'bRK(1,1); pr; 'sPC; 'sTR"of type"; 'bRK(1,1); prt; 'sPC ; 'sTR("cannot be applied to the "^term_string); 'fNL; 'sTR" "; v 0 appl; 'fNL >] |