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. --- plugins/funind/indfun.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 18817f504c..4f183b3a1d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -175,7 +175,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") + | None -> user_err "Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -391,7 +391,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl @@ -630,7 +630,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook pconstants = @@ -656,7 +656,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in let pre_hook pconstants = generate_principle (ref (Evd.from_env (Global.env ()))) -- 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. --- plugins/funind/indfun.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 4f183b3a1d..943ebc9fcb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> - errorlabstrm "" (str "Cannot find induction information on "++ + user_err "" (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with @@ -70,7 +70,7 @@ let functional_induction with_clean c princl pat = (b,a) (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) - errorlabstrm "" (str "Cannot find induction principle for " + user_err "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') @@ -321,7 +321,7 @@ let error_error names e = in match e with | Building_graph e -> - errorlabstrm "" + user_err "" (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) -- 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 --- plugins/funind/indfun.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 943ebc9fcb..61e31277f2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> - user_err "" (str "Cannot find induction information on "++ + user_err (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with @@ -70,11 +70,11 @@ let functional_induction with_clean c princl pat = (b,a) (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) - user_err "" (str "Cannot find induction principle for " + user_err (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') - | _ -> raise (UserError("",str "functional induction must be used with a function" )) + | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> princ,binding,Tacmach.pf_unsafe_type_of g princ,g @@ -175,7 +175,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err "Function" (str "Body of Function must be given") + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -321,7 +321,7 @@ let error_error names e = in match e with | Building_graph e -> - user_err "" + user_err (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) @@ -391,7 +391,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl @@ -630,7 +630,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook pconstants = @@ -656,7 +656,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let pre_hook pconstants = generate_principle (ref (Evd.from_env (Global.env ()))) @@ -834,9 +834,9 @@ let make_graph (f_ref:global_reference) = | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) end - | _ -> raise (UserError ("", str "Not a function reference") ) + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" -- cgit v1.2.3