From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 7 Jul 2016 04:56:24 +0200 Subject: Unify location handling of error functions. In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier. --- tactics/tacticals.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics/tacticals.ml') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d4..28a7b634c6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -172,14 +172,14 @@ let check_or_and_pattern_size check_and loc names branchsigns = let n = Array.length branchsigns in let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in let err1 p1 p2 = - user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in + user_err ~loc "" (str "Expects " ++ msg p1 p2 ++ str ".") in let errn n = - user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n + user_err ~loc "" (str "Expects a disjunctive pattern with " ++ int n ++ str " branches.") in let err1' p1 p2 = - user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in + user_err ~loc "" (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in let errforthcoming loc = - user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in + user_err ~loc "" (strbrk "Unexpected non atomic pattern.") in match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; @@ -508,7 +508,7 @@ module New = struct | [] -> () | (evk,evi) :: _ -> let (loc,_) = evi.Evd.evar_source in - Pretype_errors.error_unsolvable_implicit loc env sigma evk None + Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> -- cgit v1.2.3 From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- tactics/tacticals.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacticals.ml') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 28a7b634c6..c9af1f11ca 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -643,7 +643,7 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - errorlabstrm "Tacticals.general_elim_then_using" + user_err "Tacticals.general_elim_then_using" (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in -- cgit v1.2.3 From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- tactics/tacticals.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'tactics/tacticals.ml') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index c9af1f11ca..9c2dd3fee1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -172,14 +172,14 @@ let check_or_and_pattern_size check_and loc names branchsigns = let n = Array.length branchsigns in let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in let err1 p1 p2 = - user_err ~loc "" (str "Expects " ++ msg p1 p2 ++ str ".") in + user_err ~loc (str "Expects " ++ msg p1 p2 ++ str ".") in let errn n = - user_err ~loc "" (str "Expects a disjunctive pattern with " ++ int n + user_err ~loc (str "Expects a disjunctive pattern with " ++ int n ++ str " branches.") in let err1' p1 p2 = - user_err ~loc "" (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in + user_err ~loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in let errforthcoming loc = - user_err ~loc "" (strbrk "Unexpected non atomic pattern.") in + user_err ~loc (strbrk "Unexpected non atomic pattern.") in match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; @@ -311,7 +311,7 @@ module New = struct tclZERO (Refiner.FailError (lvl,lazy msg)) let tclZEROMSG ?loc msg = - let err = UserError ("", msg) in + let err = UserError (None, msg) in let info = match loc with | None -> Exninfo.null | Some loc -> Loc.add_loc Exninfo.null loc @@ -643,7 +643,7 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - user_err "Tacticals.general_elim_then_using" + user_err ~hdr:"Tacticals.general_elim_then_using" (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in -- cgit v1.2.3