Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

11 files changed, 546 insertions, 354 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 52d507a1..7e7dfd17 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -255,7 +255,7 @@ let add_new_coercion_core coef stre source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform));
+    msg_warn (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform));
   let clt =
     try
       get_target tg ind
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8f954573..85c2ca6e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -140,6 +140,6 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    warning ("Compatibility with version "^s^" not supported.");
+    msg_warn ("Compatibility with version "^s^" not supported.");
     Flags.V8_2
   | s -> Util.error ("Unknown compatibility version \""^s^"\".")
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f550df16..2ef8bd2b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -851,8 +851,8 @@ let error_same_names_overlap idl =
   str "names:" ++ spc () ++
   prlist_with_sep pr_comma pr_id idl ++ str "."
 
-let error_not_an_arity id =
-  str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity."
+let error_not_an_arity env c =
+  str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "is not an arity."
 
 let error_bad_entry () =
   str "Bad inductive definition."
@@ -888,7 +888,7 @@ let explain_inductive_error = function
   | SameNamesTypes id -> error_same_names_types id
   | SameNamesConstructors id -> error_same_names_constructors id
   | SameNamesOverlap idl -> error_same_names_overlap idl
-  | NotAnArity id -> error_not_an_arity id
+  | NotAnArity (env, c) -> error_not_an_arity env c
   | BadEntry -> error_bad_entry ()
   | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type ()
 
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 6937eeb8..46b75339 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20120710"
+let protocol_version = "20130425~2"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -22,76 +22,143 @@ type xml = Xml_parser.xml
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
 type 'a call =
-  | Interp of raw * verbose * string
-  | Rewind of int
-  | Goal
-  | Evars
-  | Hints
-  | Status
-  | Search of search_flags
-  | GetOptions
-  | SetOptions of (option_name * option_value) list
-  | InLoadPath of string
-  | MkCases of string
-  | Quit
-  | About
-
-(** The structure that coqtop should implement *)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals option;
-  evars : unit -> evar list option;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  search : search_flags -> string coq_object list;
-  get_options : unit -> (option_name * option_state) list;
-  set_options : (option_name * option_value) list -> unit;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  quit : unit -> unit;
-  about : unit -> coq_info;
-  handle_exn : exn -> location * string;
-}
+  | Interp     of interp_sty
+  | Rewind     of rewind_sty
+  | Goal       of goals_sty
+  | Evars      of evars_sty
+  | Hints      of hints_sty
+  | Status     of status_sty
+  | Search     of search_sty
+  | GetOptions of get_options_sty
+  | SetOptions of set_options_sty
+  | InLoadPath of inloadpath_sty
+  | MkCases    of mkcases_sty
+  | Quit       of quit_sty
+  | About      of about_sty
+
+type unknown
 
 (** The actual calls *)
 
-let interp (r,b,s) : string call = Interp (r,b,s)
-let rewind i : int call = Rewind i
-let goals : goals option call = Goal
-let evars : evar list option call = Evars
-let hints : (hint list * hint) option call = Hints
-let status : status call = Status
-let search flags : string coq_object list call = Search flags
-let get_options : (option_name * option_state) list call = GetOptions
-let set_options l : unit call = SetOptions l
-let inloadpath s : bool call = InLoadPath s
-let mkcases s : string list list call = MkCases s
-let quit : unit call = Quit
+let interp x      : interp_rty call      = Interp x
+let rewind x      : rewind_rty call      = Rewind x
+let goals x       : goals_rty call       = Goal x
+let evars x       : evars_rty call       = Evars x
+let hints x       : hints_rty call       = Hints x
+let status x      : status_rty call      = Status x
+let get_options x : get_options_rty call = GetOptions x
+let set_options x : set_options_rty call = SetOptions x
+let inloadpath x  : inloadpath_rty call  = InLoadPath x
+let mkcases x     : mkcases_rty call     = MkCases x
+let search x      : search_rty call      = Search x
+let quit x        : quit_rty call        = Quit x
 
 (** * Coq answers to CoqIde *)
 
-let abstract_eval_call handler c =
+let abstract_eval_call handler (c : 'a call) =
+  let mkGood x : 'a value = Good (Obj.magic x) in
   try
-    let res = match c with
-      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string)
-      | Rewind i -> Obj.magic (handler.rewind i : int)
-      | Goal -> Obj.magic (handler.goals () : goals option)
-      | Evars -> Obj.magic (handler.evars () : evar list option)
-      | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
-      | Status -> Obj.magic (handler.status () : status)
-      | Search flags -> Obj.magic (handler.search flags : string coq_object list)
-      | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
-      | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
-      | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
-      | MkCases s -> Obj.magic (handler.mkcases s : string list list)
-      | Quit -> Obj.magic (handler.quit () : unit)
-      | About -> Obj.magic (handler.about () : coq_info)
-    in Good res
+    match c with
+      | Interp x     -> mkGood (handler.interp x)
+      | Rewind x     -> mkGood (handler.rewind x)
+      | Goal x       -> mkGood (handler.goals x)
+      | Evars x      -> mkGood (handler.evars x)
+      | Hints x      -> mkGood (handler.hints x)
+      | Status x     -> mkGood (handler.status x)
+      | Search x     -> mkGood (handler.search x)
+      | GetOptions x -> mkGood (handler.get_options x)
+      | SetOptions x -> mkGood (handler.set_options x)
+      | InLoadPath x -> mkGood (handler.inloadpath x)
+      | MkCases x    -> mkGood (handler.mkcases x)
+      | Quit x       -> mkGood (handler.quit x)
+      | About x      -> mkGood (handler.about x)
   with any ->
-    let (l, str) = handler.handle_exn any in
-    Fail (l,str)
+    Fail (handler.handle_exn any)
+
+(* To read and typecheck the answers we give a description of the types,
+   and a way to statically check that the reified version is in sync *)
+module ReifType : sig
+
+  type 'a val_t
+
+  val unit_t         : unit val_t
+  val string_t       : string val_t
+  val int_t          : int val_t
+  val bool_t         : bool val_t
+  val goals_t        : goals val_t
+  val evar_t         : evar val_t
+  val state_t        : status val_t
+  val coq_info_t     : coq_info val_t
+  val option_state_t : option_state val_t
+  val option_t       : 'a val_t -> 'a option val_t
+  val list_t         : 'a val_t -> 'a list val_t
+  val coq_object_t   : 'a val_t -> 'a coq_object val_t
+  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
+  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t
+
+  type value_type = private
+    | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+    | Option of value_type
+    | List of value_type
+    | Coq_object of value_type
+    | Pair of value_type * value_type
+    | Union of value_type * value_type
+
+  val check : 'a val_t -> value_type
+
+end = struct
+
+  type value_type =
+    | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+    | Option of value_type
+    | List of value_type
+    | Coq_object of value_type
+    | Pair of value_type * value_type
+    | Union of value_type * value_type
+
+  type 'a val_t = value_type
+  let check x = x
+
+  let unit_t         = Unit
+  let string_t       = String
+  let int_t          = Int
+  let bool_t         = Bool
+  let goals_t        = Goals
+  let evar_t         = Evar
+  let state_t        = State
+  let coq_info_t     = Coq_info
+  let option_state_t = Option_state
+  let option_t x     = Option x
+  let list_t x       = List x
+  let coq_object_t x = Coq_object x
+  let pair_t x y     = Pair (x, y)
+  let union_t x y    = Union (x, y)
+
+end
+
+open ReifType
+
+(* For every (call : 'a call), we build the reification of 'a.
+ * In OCaml 4 we could use GATDs to do that I guess *)
+let expected_answer_type call : value_type =
+  let hint = list_t (pair_t string_t string_t) in
+  let hints = pair_t (list_t hint) hint in
+  let options = pair_t (list_t string_t) option_state_t in
+  let objs = coq_object_t string_t in
+  match call with
+  | Interp _     -> check (string_t                     : interp_rty      val_t)
+  | Rewind _     -> check (int_t                        : rewind_rty      val_t)
+  | Goal _       -> check (option_t goals_t             : goals_rty       val_t)
+  | Evars _      -> check (option_t (list_t evar_t)     : evars_rty       val_t)
+  | Hints  _     -> check (option_t hints               : hints_rty       val_t)
+  | Status _     -> check (state_t                      : status_rty      val_t)
+  | Search _     -> check (list_t objs                  : search_rty      val_t)
+  | GetOptions _ -> check (list_t options               : get_options_rty val_t)
+  | SetOptions _ -> check (unit_t                       : set_options_rty val_t)
+  | InLoadPath _ -> check (bool_t                       : inloadpath_rty  val_t)
+  | MkCases _    -> check (list_t (list_t string_t)     : mkcases_rty     val_t)
+  | Quit _       -> check (unit_t                       : quit_rty        val_t)
+  | About _      -> check (coq_info_t                   : about_rty       val_t)
 
 (** * XML data marshalling *)
 
@@ -113,10 +180,6 @@ let do_match constr t mf = match constr with
   else raise Marshal_error
 | _ -> raise Marshal_error
 
-let pcdata = function
-| PCData s -> s
-| _ -> raise Marshal_error
-
 let singleton = function
 | [x] -> x
 | _ -> raise Marshal_error
@@ -132,56 +195,68 @@ let bool_arg tag b = if b then [tag, ""] else []
 
 let of_unit () = Element ("unit", [], [])
 
-let to_unit = function
+let to_unit : xml -> unit = function
   | Element ("unit", [], []) -> ()
   | _ -> raise Marshal_error
 
-let of_bool b =
+let of_bool (b : bool) : xml =
   if b then constructor "bool" "true" []
   else constructor "bool" "false" []
 
-let to_bool xml = do_match xml "bool"
+let to_bool xml : bool = do_match xml "bool"
   (fun s _ -> match s with
   | "true" -> true
   | "false" -> false
   | _ -> raise Marshal_error)
 
-let of_list f l =
+let of_list (f : 'a -> xml) (l : 'a list) =
   Element ("list", [], List.map f l)
 
-let to_list f = function
+let to_list (f : xml -> 'a) : xml -> 'a list = function
 | Element ("list", [], l) ->
   List.map f l
 | _ -> raise Marshal_error
 
-let of_option f = function
+let of_option (f : 'a -> xml) : 'a option -> xml = function
 | None -> Element ("option", ["val", "none"], [])
 | Some x -> Element ("option", ["val", "some"], [f x])
 
-let to_option f = function
+let to_option (f : xml -> 'a) : xml -> 'a option = function
 | Element ("option", ["val", "none"], []) -> None
 | Element ("option", ["val", "some"], [x]) -> Some (f x)
 | _ -> raise Marshal_error
 
-let of_string s = Element ("string", [], [PCData s])
+let of_string (s : string) : xml = Element ("string", [], [PCData s])
 
-let to_string = function
+let to_string : xml -> string = function
 | Element ("string", [], l) -> raw_string l
 | _ -> raise Marshal_error
 
-let of_int i = Element ("int", [], [PCData (string_of_int i)])
+let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
 
-let to_int = function
+let to_int : xml -> int = function
 | Element ("int", [], [PCData s]) ->
   (try int_of_string s with Failure _ -> raise Marshal_error)
 | _ -> raise Marshal_error
 
-let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
+let of_pair (f : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml =
+  function (x,y) -> Element ("pair", [], [f x; g y])
 
-let to_pair f g = function
+let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
 | Element ("pair", [], [x; y]) -> (f x, g y)
 | _ -> raise Marshal_error
 
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) Util.union -> xml =
+function
+| Util.Inl x -> Element ("union", ["val","in_l"], [f x])
+| Util.Inr x -> Element ("union", ["val","in_r"], [g x])
+
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) Util.union=
+function
+| Element ("union", ["val","in_l"], [x]) -> Util.Inl (f x)
+| Element ("union", ["val","in_r"], [x]) -> Util.Inr (g x)
+| _ -> raise Marshal_error
+
 (** More elaborate types *)
 
 let of_option_value = function
@@ -275,7 +350,7 @@ let to_value f = function
         let loc_s = int_of_string (List.assoc "loc_s" attrs) in
         let loc_e = int_of_string (List.assoc "loc_e" attrs) in
         Some (loc_s, loc_e)
-      with e when e <> Sys.Break -> None
+      with Not_found | Failure _ -> None
     in
     let msg = raw_string l in
     Fail (loc, msg)
@@ -283,23 +358,24 @@ let to_value f = function
 | _ -> raise Marshal_error
 
 let of_call = function
-| Interp (raw, vrb, cmd) ->
+| Interp (id,raw, vrb, cmd) ->
   let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
-  Element ("call", ("val", "interp") :: flags, [PCData cmd])
+  Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags,
+  [PCData cmd])
 | Rewind n ->
   Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
-| Goal ->
+| Goal () ->
   Element ("call", ["val", "goal"], [])
-| Evars ->
+| Evars () ->
   Element ("call", ["val", "evars"], [])
-| Hints ->
+| Hints () ->
   Element ("call", ["val", "hints"], [])
-| Status ->
+| Status () ->
   Element ("call", ["val", "status"], [])
 | Search flags ->
   let args = List.map (of_pair of_search_constraint of_bool) flags in
   Element ("call", ["val", "search"], args)
-| GetOptions ->
+| GetOptions () ->
   Element ("call", ["val", "getoptions"], [])
 | SetOptions opts ->
   let args = List.map (of_pair (of_list of_string) of_option_value) opts in
@@ -308,37 +384,40 @@ let of_call = function
   Element ("call", ["val", "inloadpath"], [PCData file])
 | MkCases ind ->
   Element ("call", ["val", "mkcases"], [PCData ind])
-| Quit ->
+| Quit () ->
   Element ("call", ["val", "quit"], [])
-| About ->
+| About () ->
   Element ("call", ["val", "about"], [])
 
 let to_call = function
 | Element ("call", attrs, l) ->
   let ans = massoc "val" attrs in
   begin match ans with
-  | "interp" ->
-    let raw = List.mem_assoc "raw" attrs in
-    let vrb = List.mem_assoc "verbose" attrs in
-    Interp (raw, vrb, raw_string l)
+  | "interp" -> begin
+    try
+      let id = List.assoc "id" attrs in
+      let raw = List.mem_assoc "raw" attrs in
+      let vrb = List.mem_assoc "verbose" attrs in
+      Interp (int_of_string id, raw, vrb, raw_string l)
+    with Not_found -> raise Marshal_error end
   | "rewind" ->
     let steps = int_of_string (massoc "steps" attrs) in
     Rewind steps
-  | "goal" -> Goal
-  | "evars" -> Evars
-  | "status" -> Status
+  | "goal" -> Goal ()
+  | "evars" -> Evars ()
+  | "status" -> Status ()
   | "search" ->
     let args = List.map (to_pair to_search_constraint to_bool) l in
     Search args
-  | "getoptions" -> GetOptions
+  | "getoptions" -> GetOptions ()
   | "setoptions" ->
     let args = List.map (to_pair (to_list to_string) to_option_value) l in
     SetOptions args
   | "inloadpath" -> InLoadPath (raw_string l)
   | "mkcases" -> MkCases (raw_string l)
-  | "hints" -> Hints
-  | "quit" -> Quit
-  | "about" -> About
+  | "hints" -> Hints ()
+  | "quit" -> Quit ()
+  | "about" -> About ()
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -419,181 +498,216 @@ let to_coq_info = function
   }
 | _ -> raise Marshal_error
 
+let of_message_level = function
+| Debug s -> constructor "message_level" "debug" [PCData s]
+| Info -> constructor "message_level" "info" []
+| Notice -> constructor "message_level" "notice" []
+| Warning -> constructor "message_level" "warning" []
+| Error -> constructor "message_level" "error" []
+
+let to_message_level xml = do_match xml "message_level"
+  (fun s args -> match s with
+  | "debug" -> Debug (raw_string args)
+  | "info" -> Info
+  | "notice" -> Notice
+  | "warning" -> Warning
+  | "error" -> Error
+  | _ -> raise Marshal_error)
+
+let of_message msg =
+  let lvl = of_message_level msg.message_level in
+  let content = of_string msg.message_content in
+  Element ("message", [], [lvl; content])
+
+let to_message xml = match xml with
+| Element ("message", [], [lvl; content]) ->
+  { message_level = to_message_level lvl; message_content = to_string content }
+| _ -> raise Marshal_error
+
+let is_message = function
+| Element ("message", _, _) -> true
+| _ -> false
+
+let of_loc loc =
+  let start, stop = loc in
+  Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+
+let to_loc xml = match xml with
+| Element ("loc", l,[]) ->
+    (try
+      let start = List.assoc "start" l in
+      let stop = List.assoc "stop" l in
+      (int_of_string start, int_of_string stop)
+    with Not_found | Invalid_argument _ -> raise Marshal_error)
+| _ -> raise Marshal_error
+
+let to_feedback_content xml = do_match xml "feedback_content"
+  (fun s args -> match s with
+  | "addedaxiom" -> AddedAxiom
+  | "processed" -> Processed
+  | "globref" ->
+       (match args with
+       | [loc; filepath; modpath; ident; ty] ->
+            GlobRef(to_loc loc, to_string filepath, to_string modpath,
+                    to_string ident, to_string ty)
+       | _ -> raise Marshal_error)
+  | _ -> raise Marshal_error)
+
+let of_feedback_content = function
+| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+| Processed -> constructor "feedback_content" "processed" []
+| GlobRef(loc, filepath, modpath, ident, ty) ->
+    constructor "feedback_content" "globref" [
+      of_loc loc;
+      of_string filepath;
+      of_string modpath;
+      of_string ident;
+      of_string ty
+    ]
+
+let of_feedback msg =
+  let content = of_feedback_content msg.content in
+  Element ("feedback", ["id",string_of_int msg.edit_id], [content])
+
+let to_feedback xml = match xml with
+| Element ("feedback", ["id",id], [content]) ->
+  { edit_id = int_of_string id;
+    content = to_feedback_content content }
+| _ -> raise Marshal_error
+
+let is_feedback = function
+| Element ("feedback", _, _) -> true
+| _ -> false
+
 (** Conversions between ['a value] and xml answers
 
   When decoding an xml answer, we dynamically check that it is compatible
   with the original call. For that we now rely on the fact that all
   sub-fonctions [to_xxx : xml -> xxx] check that the current xml element
-  is "xxx", and raise [Marshal_error] if anything goes wrong.
-*)
-
-type value_type =
-  | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
-  | Option of value_type
-  | List of value_type
-  | Coq_object of value_type
-  | Pair of value_type * value_type
-
-let hint = List (Pair (String, String))
-let option_name = List String
-
-let expected_answer_type = function
-  | Interp _ -> String
-  | Rewind _ -> Int
-  | Goal -> Option Goals
-  | Evars -> Option (List Evar)
-  | Hints -> Option (Pair (List hint, hint))
-  | Status -> State
-  | Search _ -> List (Coq_object String)
-  | GetOptions -> List (Pair (option_name, Option_state))
-  | SetOptions _ -> Unit
-  | InLoadPath _ -> Bool
-  | MkCases _ -> List (List String)
-  | Quit -> Unit
-  | About -> Coq_info
+  is "xxx", and raise [Marshal_error] if anything goes wrong.  *)
 
 let of_answer (q : 'a call) (r : 'a value) : xml =
   let rec convert ty : 'a -> xml = match ty with
-    | Unit -> Obj.magic of_unit
-    | Bool -> Obj.magic of_bool
-    | String -> Obj.magic of_string
-    | Int -> Obj.magic of_int
-    | State -> Obj.magic of_status
-    | Option_state -> Obj.magic of_option_state
-    | Coq_info -> Obj.magic of_coq_info
-    | Goals -> Obj.magic of_goals
-    | Evar -> Obj.magic of_evar
-    | List t -> Obj.magic (of_list (convert t))
-    | Option t -> Obj.magic (of_option (convert t))
-    | Coq_object t -> Obj.magic (of_coq_object (convert t))
-    | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
+    | Unit          -> Obj.magic of_unit
+    | Bool          -> Obj.magic of_bool
+    | String        -> Obj.magic of_string
+    | Int           -> Obj.magic of_int
+    | State         -> Obj.magic of_status
+    | Option_state  -> Obj.magic of_option_state
+    | Coq_info      -> Obj.magic of_coq_info
+    | Goals         -> Obj.magic of_goals
+    | Evar          -> Obj.magic of_evar
+    | List t        -> Obj.magic (of_list (convert t))
+    | Option t      -> Obj.magic (of_option (convert t))
+    | Coq_object t  -> Obj.magic (of_coq_object (convert t))
+    | Pair (t1,t2)  -> Obj.magic (of_pair (convert t1) (convert t2))
+    | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
   in
   of_value (convert (expected_answer_type q)) r
 
 let to_answer xml (c : 'a call) : 'a value =
   let rec convert ty : xml -> 'a = match ty with
-    | Unit -> Obj.magic to_unit
-    | Bool -> Obj.magic to_bool
-    | String -> Obj.magic to_string
-    | Int -> Obj.magic to_int
-    | State -> Obj.magic to_status
-    | Option_state -> Obj.magic to_option_state
-    | Coq_info -> Obj.magic to_coq_info
-    | Goals -> Obj.magic to_goals
-    | Evar -> Obj.magic to_evar
-    | List t -> Obj.magic (to_list (convert t))
-    | Option t -> Obj.magic (to_option (convert t))
-    | Coq_object t -> Obj.magic (to_coq_object (convert t))
-    | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
+    | Unit          -> Obj.magic to_unit
+    | Bool          -> Obj.magic to_bool
+    | String        -> Obj.magic to_string
+    | Int           -> Obj.magic to_int
+    | State         -> Obj.magic to_status
+    | Option_state  -> Obj.magic to_option_state
+    | Coq_info      -> Obj.magic to_coq_info
+    | Goals         -> Obj.magic to_goals
+    | Evar          -> Obj.magic to_evar
+    | List t        -> Obj.magic (to_list (convert t))
+    | Option t      -> Obj.magic (to_option (convert t))
+    | Coq_object t  -> Obj.magic (to_coq_object (convert t))
+    | Pair (t1,t2)  -> Obj.magic (to_pair (convert t1) (convert t2))
+    | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
   in
   to_value (convert (expected_answer_type c)) xml
 
 (** * Debug printing *)
 
+let pr_unit () = ""
+let pr_string s = Printf.sprintf "%S" s
+let pr_int i = string_of_int i
+let pr_bool b = Printf.sprintf "%B" b
+let pr_goal (g : goals) =
+  if g.fg_goals = [] then
+    if g.bg_goals = [] then "Proof completed."
+    else
+      let rec pr_focus _ = function
+        | [] -> assert false
+        | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+        | (lg, rg) :: l ->
+          Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in
+      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+  else
+    let pr_menu s = s in
+    let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
+      "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
+          pr_menu goal ^ "]" in
+    String.concat " " (List.map pr_goal g.fg_goals)
+let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
+let pr_status (s : status) =
+  let path =
+    let l = String.concat "." s.status_path in
+    "path=" ^ l ^ ";" in
+  let name = match s.status_proofname with
+    | None -> "no proof;"
+    | Some n -> "proof = " ^ n ^ ";" in
+  "Status: " ^ path ^ name
+let pr_coq_info (i : coq_info) = "FIXME"
 let pr_option_value = function
-| IntValue None -> "none"
-| IntValue (Some i) -> string_of_int i
-| StringValue s -> s
-| BoolValue b -> if b then "true" else "false"
-
-let rec pr_setoptions opts =
-  let map (key, v) =
-    let key = String.concat " " key in
-    key ^ " := " ^ (pr_option_value v)
-  in
-  String.concat "; " (List.map map opts)
-
-let pr_getoptions opts =
-  let map (key, s) =
-    let key = String.concat " " key in
-    Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n"
-      key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
-  in
-  "\n" ^ String.concat "" (List.map map opts)
+  | IntValue None -> "none"
+  | IntValue (Some i) -> string_of_int i
+  | StringValue s -> s
+  | BoolValue b -> if b then "true" else "false"
+let pr_option_state (s : option_state) =
+  Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
+    s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
+let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
+let pr_coq_object (o : 'a coq_object) = "FIXME"
+let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
+let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x
 
 let pr_call = function
-  | Interp (r,b,s) ->
+  | Interp (id,r,b,s) ->
     let raw = if r then "RAW" else "" in
     let verb = if b then "" else "SILENT" in
-    "INTERP"^raw^verb^" ["^s^"]"
+    "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
   | Rewind i -> "REWIND "^(string_of_int i)
-  | Goal -> "GOALS"
-  | Evars -> "EVARS"
-  | Hints -> "HINTS"
-  | Status -> "STATUS"
+  | Goal _ -> "GOALS"
+  | Evars _ -> "EVARS"
+  | Hints _ -> "HINTS"
+  | Status _ -> "STATUS"
   | Search _ -> "SEARCH"
-  | GetOptions -> "GETOPTIONS"
-  | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
+  | GetOptions _ -> "GETOPTIONS"
+  | SetOptions l -> "SETOPTIONS" ^ " [" ^
+      String.concat ";"
+        (List.map (pr_pair (pr_list pr_string) pr_option_value) l) ^ "]"
   | InLoadPath s -> "INLOADPATH "^s
   | MkCases s -> "MKCASES "^s
-  | Quit -> "QUIT"
-  | About -> "ABOUT"
-
+  | Quit _ -> "QUIT"
+  | About _ -> "ABOUT"
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
   | Fail (_,str) -> "FAIL ["^str^"]"
-
-let pr_value v = pr_value_gen (fun _ -> "") v
-
-let pr_string s = "["^s^"]"
-let pr_bool b = if b then "true" else "false"
-
-let pr_status s =
-  let path =
-    let l = String.concat "." s.status_path in
-    "path=" ^ l ^ ";"
-  in
-  let name = match s.status_proofname with
-  | None -> "no proof;"
-  | Some n -> "proof = " ^ n ^ ";"
-  in
-  "Status: " ^ path ^ name
-
-let pr_mkcases l =
-  let l = List.map (String.concat " ") l in
-  "[" ^ String.concat " | " l ^ "]"
-
-let pr_goals_aux g =
-  if g.fg_goals = [] then
-    if g.bg_goals = [] then "Proof completed."
-    else
-      let rec pr_focus _ = function
-      | [] -> assert false
-      | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
-      | (lg, rg) :: l ->
-        Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l
-      in
-      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
-  else
-    let pr_menu s = s in
-    let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-      "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]"
-    in
-    String.concat " " (List.map pr_goal g.fg_goals)
-
-let pr_goals = function
-| None -> "No proof in progress."
-| Some g -> pr_goals_aux g
-
-let pr_evar ev = "[" ^ ev.evar_info ^ "]"
-
-let pr_evars = function
-| None -> "No proof in progress."
-| Some evars -> String.concat " " (List.map pr_evar evars)
-
+let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value =
-  match call with
-    | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
-    | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
-    | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value)
-    | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value)
-    | Hints -> pr_value value
-    | Status -> pr_value_gen pr_status (Obj.magic value : status value)
-    | Search _ -> pr_value value
-    | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value)
-    | SetOptions _ -> pr_value value
-    | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
-    | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
-    | Quit -> pr_value value
-    | About -> pr_value value
-
+  let rec pr = function
+  | Unit          -> Obj.magic pr_unit
+  | Bool          -> Obj.magic pr_bool
+  | String        -> Obj.magic pr_string
+  | Int           -> Obj.magic pr_int
+  | State         -> Obj.magic pr_status
+  | Option_state  -> Obj.magic pr_option_state
+  | Coq_info      -> Obj.magic pr_coq_info
+  | Goals         -> Obj.magic pr_goal
+  | Evar          -> Obj.magic pr_evar
+  | List t        -> Obj.magic (pr_list (pr t))
+  | Option t      -> Obj.magic (pr_option (pr t))
+  | Coq_object t  -> Obj.magic pr_coq_object
+  | Pair (t1,t2)  -> Obj.magic (pr_pair (pr t1) (pr t2))
+  | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2))
+  in
+  pr_value_gen (pr (expected_answer_type call)) value
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 7d0685b1..aa3f91bf 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -14,78 +14,20 @@ type xml = Xml_parser.xml
 
 type 'a call
 
-(** Running a command (given as a string).
-    - The 1st flag indicates whether to use "raw" mode
-      (less sanity checks, no impact on the undo stack).
-      Suitable e.g. for queries, or for the Set/Unset
-      of display options that coqide performs all the time.
-    - The 2nd flag controls the verbosity.
-    - The returned string contains the messages produced
-      by this command, but not the updated goals (they are
-      to be fetch by a separated [current_goals]). *)
-val interp : raw * verbose * string -> string call
-
-(** Backtracking by at least a certain number of phrases.
-    No finished proofs will be re-opened. Instead,
-    we continue backtracking until before these proofs,
-    and answer the amount of extra backtracking performed.
-    Backtracking by more than the number of phrases already
-    interpreted successfully (and not yet undone) will fail. *)
-val rewind : int -> int call
-
-(** Fetching the list of current goals. Return [None] if no proof is in 
-    progress, [Some gl] otherwise. *)
-val goals : goals option call
-
-(** Retrieving the tactics applicable to the current goal. [None] if there is 
-    no proof in progress. *)
-val hints : (hint list * hint) option call
-
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val status : status call
-
-(** Is a directory part of Coq's loadpath ? *)
-val inloadpath : string -> bool call
-
-(** Create a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables. *)
-val mkcases : string -> string list list call
-
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
-    proof is in progress. *)
-val evars : evar list option call
-
-(** Retrieve the list of options of the current toplevel, together with their 
-    state. *)
-val get_options : (option_name * option_state) list call
-
-(** Set the options to the given value. Warning: this is not atomic, so whenever
-    the call fails, the option state can be messed up... This is the caller duty
-    to check that everything is correct. *)
-val set_options : (option_name * option_value) list -> unit call
-
-(** Quit gracefully the interpreter. *)
-val quit : unit call
-
-(** The structure that coqtop should implement *)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals option;
-  evars : unit -> evar list option;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  search : search_flags -> string coq_object list;
-  get_options : unit -> (option_name * option_state) list;
-  set_options : (option_name * option_value) list -> unit;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  quit : unit -> unit;
-  about : unit -> coq_info;
-  handle_exn : exn -> location * string;
-}
+type unknown
+
+val interp      : interp_sty      -> interp_rty call
+val rewind      : rewind_sty      -> rewind_rty call
+val goals       : goals_sty       -> goals_rty call
+val hints       : hints_sty       -> hints_rty call
+val status      : status_sty      -> status_rty call
+val inloadpath  : inloadpath_sty  -> inloadpath_rty call
+val mkcases     : mkcases_sty     -> mkcases_rty call
+val evars       : evars_sty       -> evars_rty call
+val search      : search_sty      -> search_rty call
+val get_options : get_options_sty -> get_options_rty call
+val set_options : set_options_sty -> set_options_rty call
+val quit        : quit_sty        -> quit_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value
 
@@ -97,11 +39,18 @@ val protocol_version : string
 
 exception Marshal_error
 
+val of_call : 'a call -> xml
+val to_call : xml -> unknown call
+
+val of_message : message -> xml
+val to_message : xml -> message
+val is_message : xml -> bool
+
 val of_value : ('a -> xml) -> 'a value -> xml
-val to_value : (xml -> 'a) -> xml -> 'a value
 
-val of_call : 'a call -> xml
-val to_call : xml -> 'a call
+val of_feedback : feedback -> xml
+val to_feedback : xml -> feedback
+val is_feedback : xml -> bool
 
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : xml -> 'a call -> 'a value
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 6e9a0ee0..019f8a69 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -112,7 +112,7 @@ let coqide_cmd_checks (loc,ast) =
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
-let interp (raw,verbosely,s) =
+let interp (id,raw,verbosely,s) =
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   let loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
@@ -371,7 +371,7 @@ let eval_call c =
         (* Here we do send an acknowledgement message to prove everything went 
           OK. *)
         let dummy = Interface.Good () in
-        let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in
+        let xml_answer = Ide_intf.of_answer (Ide_intf.quit ()) dummy in
         let () = Xml_utils.print_xml !orig_stdout xml_answer in
         let () = flush !orig_stdout in
         let () = pr_debug "Exiting gracefully." in
@@ -392,20 +392,20 @@ let eval_call c =
     r
   in
   let handler = {
-    Ide_intf.interp = interruptible interp;
-    Ide_intf.rewind = interruptible Backtrack.back;
-    Ide_intf.goals = interruptible goals;
-    Ide_intf.evars = interruptible evars;
-    Ide_intf.hints = interruptible hints;
-    Ide_intf.status = interruptible status;
-    Ide_intf.search = interruptible search;
-    Ide_intf.inloadpath = interruptible inloadpath;
-    Ide_intf.get_options = interruptible get_options;
-    Ide_intf.set_options = interruptible set_options;
-    Ide_intf.mkcases = interruptible Vernacentries.make_cases;
-    Ide_intf.quit = (fun () -> raise Quit);
-    Ide_intf.about = interruptible about;
-    Ide_intf.handle_exn = handle_exn; }
+    Interface.interp = interruptible interp;
+    Interface.rewind = interruptible Backtrack.back;
+    Interface.goals = interruptible goals;
+    Interface.evars = interruptible evars;
+    Interface.hints = interruptible hints;
+    Interface.status = interruptible status;
+    Interface.search = interruptible search;
+    Interface.inloadpath = interruptible inloadpath;
+    Interface.get_options = interruptible get_options;
+    Interface.set_options = interruptible set_options;
+    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.quit = (fun () -> raise Quit);
+    Interface.about = interruptible about;
+    Interface.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e30404e1..c8292937 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -271,7 +271,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
     else
-      warning "Cannot build congruence scheme because eq is not found"
+      msg_warn "Cannot build congruence scheme because eq is not found"
   end
 
 let declare_sym_scheme ind =
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index 7b4312a3..f2a22f22 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.mli
@@ -86,8 +86,8 @@ type search_constraint =
     the flag should be negated. *)
 type search_flags = (search_constraint * bool) list
 
-(** A named object in Coq. [coq_object_qualid] is the shortest path defined for 
-    the user. [coq_object_prefix] is the missing part to recover the fully 
+(** A named object in Coq. [coq_object_qualid] is the shortest path defined for
+    the user. [coq_object_prefix] is the missing part to recover the fully
     qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
     [coq_object_object] is the actual content of the object. *)
 type 'a coq_object = {
@@ -103,10 +103,129 @@ type coq_info = {
   compile_date : string;
 }
 
-(** * Coq answers to CoqIde *)
+(** Coq unstructured messages *)
+
+type message_level =
+  | Debug of string
+  | Info
+  | Notice
+  | Warning
+  | Error
+
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
+(** Coq "semantic" infos obtained during parsing/execution *)
+type edit_id = int
+
+type feedback_content =
+  | AddedAxiom
+  | Processed
+  | GlobRef of (int*int) * string * string * string * string
+
+type feedback = {
+  edit_id : edit_id;
+  content : feedback_content;
+}
+
+(** Calls result *)
 
 type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
   | Good of 'a
   | Fail of (location * string)
+
+(* Request/Reply message protocol between Coq and CoqIde *)
+
+(** Running a command (given as its id and its text).
+    "raw" mode (less sanity checks, no impact on the undo stack)
+    is suitable for queries, or for the Set/Unset
+    of display options that coqide performs all the time.
+    The returned string contains the messages produced
+    but not the updated goals (they are
+    to be fetch by a separated [current_goals]). *)
+type interp_sty = edit_id * raw * verbose * string
+type interp_rty = string
+
+(** Backtracking by at least a certain number of phrases.
+    No finished proofs will be re-opened. Instead,
+    we continue backtracking until before these proofs,
+    and answer the amount of extra backtracking performed.
+    Backtracking by more than the number of phrases already
+    interpreted successfully (and not yet undone) will fail. *)
+type rewind_sty = int
+type rewind_rty = int
+
+(** Fetching the list of current goals. Return [None] if no proof is in
+    progress, [Some gl] otherwise. *)
+type goals_sty = unit
+type goals_rty = goals option
+
+(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+    proof is in progress. *)
+type evars_sty = unit
+type evars_rty = evar list option
+
+(** Retrieving the tactics applicable to the current goal. [None] if there is
+    no proof in progress. *)
+type hints_sty = unit
+type hints_rty = (hint list * hint) option
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+type status_sty = unit
+type status_rty = status
+
+(** Search for objects satisfying the given search flags. *)
+type search_sty = search_flags
+type search_rty = string coq_object list
+
+(** Retrieve the list of options of the current toplevel *)
+type get_options_sty = unit
+type get_options_rty = (option_name * option_state) list
+
+(** Set the options to the given value. Warning: this is not atomic, so whenever
+    the call fails, the option state can be messed up... This is the caller duty
+    to check that everything is correct. *)
+type set_options_sty = (option_name * option_value) list
+type set_options_rty = unit
+
+(** Is a directory part of Coq's loadpath ? *)
+type inloadpath_sty = string
+type inloadpath_rty = bool
+
+(** Create a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables. *)
+type mkcases_sty = string
+type mkcases_rty = string list list
+
+(** Quit gracefully the interpreter. *)
+type quit_sty = unit
+type quit_rty = unit
+
+type about_sty = unit
+type about_rty = coq_info
+
+type handle_exn_rty = location * string
+type handle_exn_sty = exn
+
+type handler = {
+  interp      : interp_sty      -> interp_rty;
+  rewind      : rewind_sty      -> rewind_rty;
+  goals       : goals_sty       -> goals_rty;
+  evars       : evars_sty       -> evars_rty;
+  hints       : hints_sty       -> hints_rty;
+  status      : status_sty      -> status_rty;
+  search      : search_sty      -> search_rty;
+  get_options : get_options_sty -> get_options_rty;
+  set_options : set_options_sty -> set_options_rty;
+  inloadpath  : inloadpath_sty  -> inloadpath_rty;
+  mkcases     : mkcases_sty     -> mkcases_rty;
+  quit        : quit_sty        -> quit_rty;
+  about       : about_sty       -> about_rty;
+  handle_exn  : handle_exn_sty  -> handle_exn_rty;
+}
+
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 006dc5ec..7653bfc4 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -851,7 +851,7 @@ let check_rule_productivity l =
     error "A recursive notation must start with at least one symbol."
 
 let is_not_printable = function
-  | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
+  | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true
   | _ -> false
 
 let find_precedence lev etyps symbols =
@@ -909,7 +909,7 @@ let remove_curly_brackets l =
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
                   if l <> l0 or l' <> l1 then
-                    warning "Skipping spaces inside curly brackets";
+                    msg_warn "Skipping spaces inside curly brackets";
                   if deb & l'' = [] then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index f08308d3..b6639c06 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -117,7 +117,7 @@ let dir_ml_load s =
 let dir_ml_use s =
   match !load with
     | WithTop t -> t.use_file s
-    | _ -> warning "Cannot access the ML compiler"
+    | _ -> msg_warn "Cannot access the ML compiler"
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
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