diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 75efe139..e7db8fac 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -801,7 +801,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (System.expand_path_macros path) - with Sys_error str -> warning ("Cd failed: " ^ str) + with Sys_error str -> msg_warn ("Cd failed: " ^ str) end; if_verbose message (Sys.getcwd()) @@ -883,6 +883,12 @@ let vernac_declare_arguments local r l nargs flags = | x, _ -> x in List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let renamed_arg = ref None in + let set_renamed a b = + if !renamed_arg = None && a <> b then renamed_arg := Some(b,a) in + let pr_renamed_arg () = match !renamed_arg with None -> "" + | Some (o,n) -> + "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try Arguments_renaming.arguments_names sr <> names_decl with Not_found -> false in @@ -894,15 +900,19 @@ let vernac_declare_arguments local r l nargs flags = | (Name x, _,_, true, _), Anonymous -> error ("Argument "^string_of_id x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> + set_renamed iid id; b || iid <> id, Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> b || iid <> id, None + | (Name iid, _,_, _, _), Name id -> + set_renamed iid id; + b || iid <> id, None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', Util.list_map_filter (fun x -> x) impl) some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error "To rename arguments the \"rename\" flag must be specified." + error ("To rename arguments the \"rename\" flag must be specified." + ^ pr_renamed_arg ()) else Arguments_renaming.rename_arguments local sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in |