summaryrefslogtreecommitdiff
path: root/toplevel/class.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /toplevel/class.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml13
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 92fd2d4c..2c6a63b0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: class.ml 11085 2008-06-10 08:54:43Z herbelin $ *)
+(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Pp
@@ -119,7 +119,7 @@ let class_of_global = function
| ConstructRef _ as c ->
errorlabstrm "class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
- str " cannot be used as class")
+ str ", cannot be used as a class.")
(*
lp est la liste (inverse'e) des arguments de la coercion
@@ -189,7 +189,7 @@ let ident_key_of_class = function
let error_not_transparent source =
errorlabstrm "build_id_coercion"
- (pr_class source ++ str " must be a transparent constant")
+ (pr_class source ++ str " must be a transparent constant.")
let build_id_coercion idf_opt source =
let env = Global.env () in
@@ -218,8 +218,8 @@ let build_id_coercion idf_opt source =
(Reductionops.is_conv_leq env Evd.empty
(Typing.type_of env Evd.empty val_f) typ_f)
then
- error ("cannot be defined as coercion - "^
- "maybe a bad number of arguments")
+ errorlabstrm "" (strbrk
+ "Cannot be defined as coercion (maybe a bad number of arguments).")
in
let idf =
match idf_opt with
@@ -283,7 +283,8 @@ let add_new_coercion_core coef stre source target isid =
let try_add_new_coercion_core ref b c d e =
try add_new_coercion_core ref b c d e
with CoercionError e ->
- errorlabstrm "try_add_new_coercion_core" (explain_coercion_error ref e)
+ errorlabstrm "try_add_new_coercion_core"
+ (explain_coercion_error ref e ++ str ".")
let try_add_new_coercion ref stre =
try_add_new_coercion_core ref stre None None false