From 0b1c4218edbe9c1e43b0b62941905ed2c7d7a848 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 Nov 2000 15:59:09 +0000
Subject: amélioration

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@827 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 8 ++++----
 1 file 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 >]
-- 
cgit v1.2.3