The command has indeed failed with message:
Flag "rename" expected to rename A into B.
File "stdin", line 3, characters 0-25:
Warning: This command is just asserting the names of arguments of identity.
If this is what you want, add ': assert' to silence the warning. If you want
to clear implicit arguments, add ': clear implicits'. If you want to clear
notation scopes, add ': clear scopes' [arguments-assert,vernacular]
@eq_refl
     : forall (B : Type) (y : B), y = y
eq_refl
     : ?y = ?y
where
?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

Arguments eq {A}%type_scope
Arguments eq_refl {B}%type_scope {y}, [B] _
eq_refl : forall {A : Type} {x : A}, x = x

eq_refl is not universe polymorphic
Arguments eq_refl {B}%type_scope {y}, [B] _
Expands to: Constructor Coq.Init.Logic.eq_refl
Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x

Arguments myEq _%type_scope
Arguments myrefl {C}%type_scope x : rename
myrefl : forall {B : Type} (x : A), B -> myEq B x x

myrefl is not universe polymorphic
Arguments myrefl {C}%type_scope x : rename
Expands to: Constructor Arguments_renaming.Test1.myrefl
myplus = 
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S n' => S (myplus T t n' m)
  end
     : forall T : Type, T -> nat -> nat -> nat

Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
myplus : forall {T : Type}, T -> nat -> nat -> nat

myplus is not universe polymorphic
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
The reduction tactics unfold myplus when the 2nd and
  3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Arguments_renaming.Test1.myplus
@myplus
     : forall Z : Type, Z -> nat -> nat -> nat
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
    myrefl : B -> myEq A B x x

Arguments myEq (_ _)%type_scope
Arguments myrefl A%type_scope {C}%type_scope x : rename
myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x

myrefl is not universe polymorphic
Arguments myrefl A%type_scope {C}%type_scope x : rename
Expands to: Constructor Arguments_renaming.myrefl
myrefl
     : forall (A C : Type) (x : A), C -> myEq A C x x
myplus = 
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S n' => S (myplus T t n' m)
  end
     : forall T : Type, T -> nat -> nat -> nat

Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
myplus : forall {T : Type}, T -> nat -> nat -> nat

myplus is not universe polymorphic
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
The reduction tactics unfold myplus when the 2nd and
  3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Arguments_renaming.myplus
@myplus
     : forall Z : Type, Z -> nat -> nat -> nat
The command has indeed failed with message:
Argument lists should agree on the names they provide.
The command has indeed failed with message:
Sequences of implicit arguments must be of different lengths.
The command has indeed failed with message:
Some argument names are duplicated: F
The command has indeed failed with message:
Argument number 3 is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
The command has indeed failed with message:
Extra arguments: y.
The command has indeed failed with message:
Flag "rename" expected to rename A into R.