From 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 15 Mar 2017 20:48:10 +0100 Subject: [cleanup] Unify all calls to the error function. This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated. --- library/declaremods.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 3a263b1e1..08c33b5c1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -345,7 +345,7 @@ let get_applications mexpr = let rec get params = function | MEident mp -> mp, params | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> error "Non-atomic functor application." + | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") in get [] mexpr (** Create the substitution corresponding to some functor applications *) @@ -353,7 +353,7 @@ let get_applications mexpr = let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst - | [],r -> error "Application of a functor with too few arguments." + | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in @@ -777,7 +777,7 @@ let rec decompose_functor mpl typ = match mpl, typ with | [], _ -> typ | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> error "Application of a functor with too much arguments." + | _ -> user_err Pp.(str "Application of a functor with too much arguments.") exception NoIncludeSelf -- cgit v1.2.3