diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 13 |
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 |