Copy array before updating. Fixes weird issue with undo

[amosr]

Hello, I found an issue where reflect_arith in CoqIde wasn't undoing properly. So if I applied reflect_arith, went back one step, I would still have the eval stuff, then I could apply it again and get two levels of evals. It turned out it was modifying the arguments.

The error goes something like this (although I was using coqide not coqtop and didn't test coqtop):

Coq < Goal forall a b, a + b + 1 = 0.
1 subgoal

  ============================
  forall a b : nat, a + b + 1 = 0

Unnamed_thm < intros.
1 subgoal

  a, b : nat
  ============================
  a + b + 1 = 0

Unnamed_thm < reflect_arith.
1 subgoal

  a, b : nat
  ============================
  eval (b :: (a :: nil)%list)
    (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1)) =
  eval (b :: (a :: nil)%list) (a_const 0)

Unnamed_thm < Back.
1 subgoal

  a, b : nat
  ============================
  eval (b :: (a :: nil)%list)
    (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1)) =
  eval (b :: (a :: nil)%list) (a_const 0)

Unnamed_thm < reflect_arith.
1 subgoal

  a, b : nat
  ============================
  eval
    (eval (b :: (a :: nil)%list)
       (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1))
     :: (eval (b :: a :: nil) (a_const 0) :: nil)%list)
    (a_var 0) =
  eval
    (eval (b :: (a :: nil)%list)
       (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1))
     :: (eval (b :: a :: nil) (a_const 0) :: nil)%list)
    (a_var 1)