List.rev is unexpectedly quadratic

This is probably known to a number of Coq developers, but I discovered only yesterday, after 15 years of using Coq, that List.rev is implemented with quadratic complexity. That could explain numerous of the performance bottleneck that I, and others, have encountered.

I then saw that Coq.Lists.List also defines a rev' function, with the proper tail-rec definition. But I don't recall seeing it used in any Coq script that I have looked at.
I suggest to better advertise the issue with the definition of rev. At the very least, I guess there should be a comment above the definition of rev, and possibly also at the top of the file.

Another possibility for tracking down problematic usages would be to develop a profiler version for coqc , that could, among other things, measure the length of arguments of rev and report a warning whenever the length exceeds a couple dozen elements. Such a profiler could be exploited by users who want their scripts to run faster, suggesting hints for improvements.

To see how bad the quadratic behavior gets in practice, I ran the following benchmark. Even for short lists, the computation time is significant.

Set Implicit Arguments.
From Coq Require Import List.

Fixpoint make A (n:nat) (v:A) : list A :=
   match n with
   | 0 => nil
   | S n' => v :: make n' v
   end.

Set Implicit Arguments.
From Coq Require Import List.

Fixpoint make A (n:nat) (v:A) : list A :=
   match n with
   | 0 => nil
   | S n' => v :: make n' v
   end.

Lemma test : forall (v w:nat),
      last (rev (make 300 v)) w = v
  /\  last (rev (make 500 v)) w = v
  /\  last (rev (make 500 v)) w = v
  /\  last (rev (make 1500 v)) w = v
  /\  last (rev (make 5000 v)) w = v
  /\  last (rev' (make 5000 v)) w = v.
Proof. 
  intros. split;[|split;[|split;[|split;[|split]]]].
  time simpl. auto.  (* >1 second for 300 elements *)
  time simpl. auto.  (* 5 seconds for 500 elements *)
  time reflexivity. (* 0.1 seconds for 500 elements *)
  time reflexivity. (* >1 seconds for 1500 elements *)
  time reflexivity. (* 17 seconds for 5000 elements *) 
  time reflexivity. (* 0.01 seconds for 5000 elements with the tail rec version *) 
Abort.

Start with the Coq.Lists.List definitions of rev and rev' and review the benchmark in the issue. Clarify the complexity difference and document it near rev or at the top of the module; done means users can discover that rev is quadratic and rev' is tail-recursive.