Cleaning, documentation, uniformisation of the Coq extension of List.

Still some discrepancies though. E.g.:
- some functions taking an equality as arguments have suffix `_f` but
  not all;
- the functions possibly raising an error have still different kinds
  of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange,
  and when in the first two cases, with no unique rules in the style
  of the associated string - we thus avoid to document the exact
  string used).

There are a few semantics changes:
- skipn_at_least now raises a `Failure` if its argument is negative;
- map3 raises an Invalid_argument "List.map3" rather than
  Invalid_argument "map3" and similarly for map4
- internally, map3 and map4 are now tail-recursive (by uniformity);
- internally, split3 and combine3 are now tail-recursive (by uniformity);
- filter is now "smart" by default and smartfilter is deprecated;
- smartmap is now tail-recursive by default.

1 files changed, 2 insertions, 2 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index a86103d57..d3acb5aa5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -672,7 +672,7 @@ struct
 
   let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
 
-  let remove_sdl p sdl = List.Smart.filter p sdl
+  let remove_sdl p sdl = List.filter p sdl
 
   let remove_he st p se =
     let sl1' = remove_sdl p se.sentry_nopat in
@@ -684,7 +684,7 @@ struct
     let filter (_, h) =
       match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
-    let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+    let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
   let remove_one gr db = remove_list [gr] db